When the Compiler Knows What You Owe: Obligations as a Capability Oracle

· 6 min read

The Mortality Law · part 2 of 3 — part 1: the wall, measured in Mojo · part 3: outcomes as control flow.

Here are four real diagnostics from the Koru compiler, all the same error code (KORU030), all “you abandoned a resource,” and all saying something different (line-wrapped here — the compiler emits each on one line):

error[KORU030]: Resource '_' carries obligation <open!> was not discharged.
                Call one of: app.db:begin

error[KORU030]: Resource '*Transaction' obligation <started!> was not discharged.
                Call one of: tx.exec

error[KORU030]: Resource '*Transaction' obligation <active!> was not discharged.
                Call one of: tx.rollback, tx.commit

error[KORU030]: Resource '_' carries obligation <active!> was not discharged.
                Call one of: app.db:close, app.db:tx.begin

Read them as a transcript, not as errors. A fresh connection: exactly one legal continuation — begin. A started transaction: exactly one — exec. An active transaction: two — commit or rollback, surfaced as a decision point, not picked for you. A post-commit connection: close it or start another transaction.

The list is not a hint and not documentation. It is computed — the checker derives, from the phantom atoms the value currently carries, which declared events can legally consume it. Change the state, and the next-move list changes with it.

Progressive disclosure, enforced

An agent harness wants to disclose capabilities progressively: hand the agent file.open, get back a handle, and let the handle say what it can do next — rather than front-loading the entire API surface into context and hoping the model doesn’t improvise outside it.

That is precisely what this diagnostic is. The obligation atoms (open!, started!, active!) ride the type; each transition the agent performs re-derives the currently-legal moves. The refusal is the documentation — precise to the state the program is actually in, and incapable of drifting from the truth, because it’s produced by the same algebra that enforces it.

Three properties fall out that are usually engineering projects of their own:

  • Termination is machine-checkable. “Is this session done?” = “are all obligations discharged?” An agent cannot declare victory while holding a dangling handle — the program simply does not compile. The outstanding atoms are a to-do list the compiler maintains and the agent cannot gaslight.
  • Decisions are disclosed as decisions. When two verbs discharge the same obligation (commit XOR rollback), the error lists both. The compiler reports that a choice exists and declines to make it — except when there’s exactly one continuation, where Koru can synthesize the discharge: a dropped committed connection gets a close() the programmer never wrote.
  • The audit trail is the binary. Every resource’s death is either authored in the text or provably inserted. There is no third state.

Why this needed an algebra, not a flag

We measured the alternative this week. Mojo ships a genuinely strong version of the enforcement half — Deinitable where False makes a value undroppable, tracked across returns, branches, raises, containers, existentials, and copies; we threw twelve probes at it and the wall held. But its diagnostic is an author-written string:

@explicit_destroy("Transaction must be finished via .commit() or .rollback()")
struct Tx[active: Bool](Deinitable where False, Movable):

One fixed message per type — the same text whether you hold Tx[False] or Tx[True], and unchecked against the method table. Mojo cannot print “call tx.exec” because nothing connects exec to the obligation; consuming methods are just methods that take deinit self, and a method that consumes while releasing nothing compiles clean — the compiler knows that a value died, never what the death meant. Koru’s list is correct by construction: a verb only appears if the algebra says it discharges the atom.

That is the difference the word “algebra” buys. A one-bit flag (not Deinitable) can answer “does this owe a death?” An obligation count with named atoms can answer what do I hold, what must I do, what may I do — at every program point, per handle, per state. Progressive disclosure needs the second answer. A bit can’t give it.

Where the limits are

Honesty section, because the claim is only as good as its edges:

  • The disclosure is exactly as good as the vocabulary. The atoms and verbs are declared by the protocol author (db.kz in the corpus); a bad atom set produces bad guidance. This is a design surface, not a mechanism gap — but it’s real authorship work.
  • It covers what the types carry. Ordinary values have no obligations and disclose nothing; the oracle answers only for declared resources.
  • The mechanism is the flow checker’s, not magic. The lists above are verbatim KORU030 output from the transaction-protocol corpus — every cell of that corpus is a compiled program in the repo.

All of it is pinned and reproducible — the abandoned-transaction cases, the evolving call-lists, the synthesized close():

The agent-harness direction writes itself from here: the vocabulary is the capability manifest, the compiler is the oracle that keeps it honest, and the error channel is the wire the disclosure travels on. We measured that the enforcement exists. This post is the claim that the enforcement is queryable — and that the query is the product.