Poly – A human readable programming language for Coding Agents

A programming language and runtime for the stateful core of software written by coding agents.

A poly program is a set of declared state machines. Each machine carries its contract, its invariants, its effects and the obligations that govern it. The compiler checks the program exhaustively over declared finite domains before it may run. The runtime executes the same program durably, gates every effect, and writes a ledger that replays exactly.

poly adds no new checking, simulation or governance engine. It is a compiler, a toolchain and one runtime integration over the Poly stack. Every construct lowers to an artefact an existing engine already reads:

Status: specification, draft v0.6 (after five reviews). No code yet.

A turnstile. Put a coin in, it unlocks; push it, it locks.

module hello

type Mode = Locked | Unlocked

machine Gate {
  state {
    mode  : Mode = Locked
    coins : 0..3 = 0
  }
  action Coin()
  action Push()

  on Coin {
    require coins < 3 else reject "coin-box-full"
    coins' = coins + 1
    mode' = Unlocked
  }
  on Push {
    require mode is Unlocked else reject "locked"
    mode' = Locked
  }

  invariant locked-when-empty: coins == 0 implies mode is Locked
}
bash
$ poly check hello.poly
hello.poly:5  PL3201 DEADLOCK  Gate
  no action is accepted in a reachable non-terminal state
  witness (4 steps):
    Coin()   Locked/0   -> Unlocked/1
    Coin()   Unlocked/1 -> Unlocked/2
    Coin()   Unlocked/2 -> Unlocked/3
    Push()   Unlocked/3 -> Locked/3      then Coin: coin-box-full, Push: locked
verdict: FINDINGS (exit 1)  over coins ∈ 0..3; 7 states

The invariant holds. What poly check finds is that a full coin box locks the turnstile forever. Add an operator action and it is clean:

  action Empty()
  on Empty {
    require mode is Locked else reject "unlocked"
    coins' = 0
  }

Running it from TypeScript takes three lines:

const rt = await load('./.poly/build')
const gate = await rt.create('hello.Gate')
await rt.dispatch(gate.id, 'Coin', {}, { actionId: 'coin-1' })   // { stepKind: 'accepted', state: { mode: 'Unlocked', coins: 1 } }

Handlers are pure functions of the pre-state: a primed field is written, never read. That is why the order of lines inside a handler cannot change what it does. The same machine can also be written as TypeScript with the embedded surface (technical specification, PT2.5).

machine Order {
  state {
    status : Status = Draft
    items  : 0..3   = 0
    paid   : bool   = false
  }
  action AddItem()
  action Place()
  action Pay(amount: int check { 10, 20 })

  on Place {
    require status == Draft else reject "not-draft"
    require items > 0      else reject "empty-order"
    status' = Placed
  }
  on Pay(amount) {
    require status == Placed else reject "not-placed"
    emit charge(amount)
  }

  invariant shipped-was-paid: status == Shipped implies paid
  path property charge-at-most-once: count("payment.charge") <= 1

  effect charge(amount: int) {
    kind "payment.charge"
    labels { egress:external }
    class irreversible
    ok -> PaymentOk()
    failed -> PaymentFailed(code: "declined")
  }
}

poly check finds that two Pay calls emit two charges, and says why they can:

orders.poly:17  PL4001 PATH_PROPERTY  charge-at-most-once
  witness (4 steps):
    AddItem()      Draft/0  -> Draft/1
    Place()        Draft/1  -> Placed/1
    Pay(10)        Placed/1 -> Placed/1   emits payment.charge
    Pay(10)        Placed/1 -> Placed/1   emits payment.charge   <- count = 2
  test:  poly witness sha256:3be1… --test   (fails on this program)
  fixes: [enter-charging-status]  add status Charging, entered by Pay, left by PaymentOk / PaymentFailed
orders.poly:16  PL4002 EMIT_WITHOUT_STATE_CHANGE  Pay
  Pay emits payment.charge and leaves the state unchanged, so it can repeat its effect without limit
  witness (4 steps):
    AddItem()      Draft/0  -> Draft/1
    Place()        Draft/1  -> Placed/1
    Pay(10)        Placed/1 -> Placed/1   emits payment.charge
    Pay(10)        Placed/1 -> Placed/1   emits payment.charge
  fixes: [enter-charging-status]  record the emission in the state
verdict: FINDINGS (exit 1)  over items ∈ 0..3, amount ∈ {10, 20}

Each call is allowed; the sequence is not. The second finding names the cause: a step that emits and changes nothing can always be taken again. That is the bug the Poly stack was built to find, reported before the program can run. The snippet is abridged; the full example is in the technical specification, PT4.5.

Machines hold addresses, not each other's state, and talk only by send. A configuration checks several of them together, with messages arriving in any order. In the checkout example (technical specification, PT7a), an inventory and each order are safe on their own. If the order confirms as soon as it hears "available", two orders can both be confirmed against the last unit:

checkout.poly:33  PL5401 CONFIGURATION_INVARIANT  confirmed-within-stock
  witness: Place@order[0], Place@order[1], Query(order[0]) -> inv, Query(order[1]) -> inv,
           Available(1) -> order[0], Available(1) -> order[1]

No per-machine check can see this. The defect lives in the arrival order between machines.

The semantics is the definition. 04-semantics says what a program means; everypoly check validates the lowering against it. 0a.One program, three interpreters. The same machine is checked (all inputs), simulated (sampled inputs, v2) and run (real inputs). Only the environment changes. 0b.Machines talk only by messages. Addresses are values,send is the only way to affect a peer, and interacting machines are checked together as configurations. 2. The engines check single machines; poly checks how machines relate. Safety, governance, simulation and mining stay in the engines. poly's own model checker, poly-ref, checks the lowering, deadlock, liveness and configurations. 3. The checked program is the running program, over its check domains. A certificate binds the source, the artefacts and the check results by digest. Out-of-domain inputs are rejected (strict ) or journaled as drift (disclosed ).Domains refuse by default (S400, PT3.4a). A check domain on an action's parameter is a constraint: an integer range, an enum, abool or acheck { … } clause refuses a value outside it at dispatch, with the reasonoutside-check-domain , before the handler runs. Writedisclosed after acheck clause (amount: int check { 1, 2 } disclosed ) to accept values outside the domain and only report them; such a value is then outside what was checked. 4. One source per machine. Every engine artefact is derived. 5. No silent clean. Every check reports clean, findings, refused, underpowered or inconclusive. 6. No model call on a check or decision path. 7. The journal is the corpus. Runtime journals feed replay, versioning, mining and simulation unchanged.

The Poly stack already holds the primitives a coding agent needs to write stateful code that holds. poly makes them one language. The first milestone is a lowering that reproduces the field-study results from poly source. The third is an experiment, run before any runtime is built, that measures escaped defects and cost against the host language alone. The runtime work depends on its result.