Pactern Language: Delegate the code. Keep the contract

Andrew Arrow released Pactern 0.1.0, a developer-preview programming language for AI-written backend components in which an external baseline called a pact defines acceptable behavior separately from the implementation, so agents can change code while the requirement stays fixed. The toolchain checks signatures, effects, arithmetic safety and termination, runs guarded C/Wasm with bounded memory, and rejects stale or weakened edits; static Z3 proof covers only a loop-free pure fragment, loops and recursion remain unsupported, storage is in-memory, and agent productivity gains have not been measured.

Requirements survive edits. An external baseline protects pacts and their meaning-defining helpers. Both text edits and semantic requests face the acceptance gate. Changing a requirement needs approval tied to the exact diff. Protected changes https://github.com/andrewarrow/pactern/blob/main/docs/semantic.md 0.1.0 · Developer preview Delegate the code. Keep the contract. A programming language for AI-written backend components. You define the requirements. Agents change the implementation. The toolchain checks the agreement. A repair with a fixed target A green build means less if an agent also rewrites the expected result. A pact states acceptable behavior separately, so the implementation can change while the requirement stays put. src/quota.ptn · function excerpt php pub fn reserve available: I64, amount: I64 - Result<I64, ReserveError { if amount <= 0 { return Result::Err ReserveError::InvalidAmount ; } if amount available { return Result::Err ReserveError::InsufficientQuota ; } return Result::Ok available - amount ; } Check before subtracting. The repair rejects invalid amounts and insufficient quota. A valid reservation still has to succeed: returning an error for every request would also violate the pact. 3 4 Err InsufficientQuota Same pact in both cases. The verifier also checks arithmetic safety and termination separately. A useful pact describes acceptable results independently of the algorithm. For quotas, worker allocation, or validation, a few stable properties can constrain many implementations. The pact itself still needs human review. Beyond a function contract The executable quota workflow connects inspection, verification, protected edits, sandboxed execution, and replay. Inspect signatures, callers, effects, and affected pacts through the semantic API. Stage an edit against persistent symbol IDs and a workspace revision. Managed snapshots commit atomically; stale proposals are rejected. Effect declarations expose requested operations. Host-issued, noncopyable handles grant tenant-scoped access. The Wasm host bounds memory and execution; the quota adapter enforces transactions, budgets, and cleanup. Proofs, runtime guards, and executed tests have separate results bound to source, tools, policy, and artifact hashes. Quota traces replay against their recorded revision with zero live writes. Unknown and unsupported remain explicit. Expose the defect, reject a weakened pact, apply a proof-gated repair, reject a stale change, and replay the original failure. cargo run -p pactern --locked \ --example quota workflow -- target/quota-workflow A scripted demonstration. Outputs include generated C/Wasm, traces, repair receipts, and artifact-linked evidence. Where to use it first Start with business rules, validation, data transformations, and bounded jobs called by an existing application. Functions, records, enums, generics, Option and Result . Immutable values by default. Explicit local mutation. Checked signed 64-bit arithmetic. .ptn sourceRust toolchainGenerated CWebAssembly The interpreter, C backend, and verifier consume the same typed core representation. Source checking and formatting, effect and handle checks, guarded C/Wasm execution, seeded property tests, narrow Z3 verification, semantic queries, managed edits, and the transactional quota/replay host. Static proof covers a loop-free pure fragment; loops and recursion remain unsupported by the verifier. Invocation arguments are specialized into each Wasm artifact. Storage is in-memory. A complete LSP extension and external CI activation remain open. Agent productivity gains have not been measured. This is an experimental developer preview. Build it. Check it. Run it. Build from source, then reserve two units from a balance of three. The CLI compiles the quota function and its pact to guarded Wasm and runs it in the bounded host. Use the pinned Rust toolchain via rustup. Compiled execution needs Clang and wasm-ld; verification also needs Z3. Exact versions and setup are in the candidate guide. git clone https://github.com/andrewarrow/pactern.git cd pactern cargo build --workspace --locked cd fixtures/conformance ../../target/debug/pactern run \ --entry quota::reserve --args ' "3","2" ' \ src/quota.ptn contracts/quota.pact.ptn --json Result Result::Ok 1 One unit remains. ../../target/debug/pactern verify \ src/quota.ptn contracts/quota.pact.ptn --json I64 arguments use JSON decimal strings to preserve their exact value.