Mojo's Mortality Law: Forced Discharge in Python Syntax, Verified Against the Compiler

The Mortality Law · part 1 of 3 — part 2: when the compiler knows what you owe · part 3: outcomes as control flow.

A Mojo program that opens a transaction and never finishes it does not compile. Not a lint, not a warning you can silence — a hard error, on every control-flow edge, in every function the value flows through. This is Python-family syntax — def, var, decorators, no unsafe blocks, no lifetime annotations — enforcing a guarantee that Rust’s ownership system deliberately cannot express: this resource must be explicitly discharged, or the program does not exist.

We did not take the documentation’s word for it. The mechanism was read out of the compiler source, then measured by compiling the full transaction-protocol corpus under Mojo 1.2.0.dev2026091605 and probing every escape hatch we could think of. The wall is real. This post is about where it stands and — completely honestly — where it ends.

The mechanism is stranger than the reputation

Mojo does not have a linear type system in the textbook sense. Reading CheckLifetimes.cpp (~5.7k lines, in the Modular source checkout at 64fcd68) shows a universal mortality law: every value must die, destruction is placed at last-use rather than scope end, and liveness is tracked by per-field bitvector dataflow on every CFG edge. “Linear” is the name for the types the law cannot kill itself.

Linearity is defined negatively. A type conforms to Deinitable by default; spelling Deinitable where False removes the compiler’s legal destructor, and from then on the value can only die by a named deinit method — and a type can have several, which is commit-XOR-rollback as a primitive:

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

    def __init__(out self, conn_handle: Int):
        self.conn_handle = conn_handle

    def exec(deinit self, sql: String) -> Tx[True]:
        print("Executing:", sql)
        return Tx[True](self.conn_handle)

    def commit(deinit self) -> Connection[True] where Self.active:
        print("COMMIT")
        return Connection[True](self.conn_handle)

    def rollback(deinit self) -> Connection[True] where Self.active:
        print("ROLLBACK")
        return Connection[True](self.conn_handle)

Read it as a state machine: exec consumes a Tx[False] and returns a Tx[True]; commit and rollback are where Self.active-gated so a never-executed transaction cannot legally die by them. x^.commit() transfers ownership in. None of this is exotic notation — it is def and struct and one where clause. The entire enforcement apparatus is invisible in the source except where the type author opted in.

It survives the program, not just the scope

The debt rides the type, so it follows the value anywhere the value can legally go. Twelve probes, all compiled:

The stdlib runs on this law itself: Allocation is @explicit_destroy-marked — “must be consumed before it goes out of scope… prevents accidental leaks and double-frees” — and the escape hatch is honestly named unsafe_leak().

Measured against the corpus, not against prose

The instrument for this is the 2104_* shootout corpus: twenty-two programs of one protocol — open a connection, begin a transaction, execute work, commit XOR rollback, close — each a different way to get it right or wrong, each already compiled under Koru and under Rust. The first Mojo batch is nine cases:

Every Rust cell reading “builds, panics at drop” is a hand-written Drop guard catching the mistake in a binary that already shipped. Mojo’s refusals need no guard:

error: 'tx' abandoned without being explicitly destroyed:
Transaction must be finished via .commit() or .rollback()

Where it ends — completely honestly

Two edges, both now measured rather than predicted, and both are structural rather than bugs.

Raw memory is outside the law. unsafe_write a linear Tx into a heap Allocation, then dealloc the storage: compiles, runs, exit 0. The payload’s death is never checked. The fence is honest — every step is unsafe_-named — but the hole is real: a value that leaves the tracked world takes its obligation with it, and the freed storage answers for nothing. This is the same wall every such system hits; Mojo’s is just clearly marked.

The law knows that a value died, never what the death meant. A deinit method that consumes the channel and releases nothing — a “use” that re-issues the obligation in name only — compiles and runs clean. There is no obligation count for the checker to consult: the value is the debt, so consume-and-reissue and consume-and-release are the same shape to it. The verb list in the diagnostic is author-written @explicit_destroy text, not a derivation. Koru’s checker reads the return-type atoms and computes which verbs discharge — which is why it can also synthesize the discharge: 2104_15’s dropped connection gets a close() the programmer never wrote, the one row Mojo cannot match without flipping its whole regime to always-auto. What the derivation buys beyond a better error message — a diagnostic that can enumerate the currently-legal moves, per obligation state, and why that matters for an agent harness doing progressive disclosure — is its own post: when the compiler knows what you owe.

Two smaller ones, for completeness: an obligation cannot ride a foreign type (string<open!> has no spelling — conformance is declared at the type, and the wrapper that stands in leaks its payload back out obligation-free), and ordered discharge is expressible — one more phantom parameter per step — rather than counted.

The line

Mojo is not a slouch. A language with Python’s surface is shipping the strongest enforced-ownership guarantee we have measured in a production compiler — forced discharge that survives scope, containers, existentials, and copies, with the only escapes clearly fenced behind unsafe. It enforces mortality perfectly. What it cannot do is account for what the death meant — and that is precisely the layer where obligations stop being a law and start being a currency.

All of it is in the repo: nine verdict files with commands and verbatim compiler output, twelve probe programs, and the mapping — Deinitable where False for <!atom>, where Self.active for the state gate, deinit self -> T[…] for the re-issue. Reproduce any cell yourself; the toolchain is one pixi install away.