Pactern Language: Delegate the code. Keep the contract

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

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

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

ResultResult::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.