Verification

The last redefinition. Formal verification is usually a separate world — a separate language, a separate tool, an all-or-nothing switch. Makoto folds it into the one language as a spectrum you climb.

The idea

“Verification” in most of the industry means one of two extremes. Either you have nothing — the type checker catches shape errors and everything else is a test, a runtime panic, or a production incident — or you go to the other end and adopt a proof assistant (Coq, Agda, Lean, Idris), a separate language with a separate mental model, where verifying anything means verifying in that world and then somehow bridging back. The middle is thinly populated: a refinement here, a linter there, rarely composing.

Makoto starts from a different premise: a systems language that promises resilience owes the programmer a way to state a guarantee and have the compiler earn it — and that way should be the same language, summoned in fragments, priced per fragment.

How Makoto redefines it

Verification is not a mode; it is a ladder. Every guarantee is the same shape — an obligation on a predicate — and the compiler discharges each obligation as high as it will go: unrepresentable in the type if it can be, folded at comptime if the values are known, proven by a summoned solver if arithmetic demands it, checked at runtime if it must be, and, at the very bottom, asserted by a human who signs for it. The one law is that an obligation that cannot be met at a rung falls to the next rung down, never off the ladder. A guarantee never silently disappears; it degrades, visibly, to the strongest honest form that remains.

From that single image everything else follows. Ownership disciplines (@must_consume, @consume_once), refinements (@where), session protocols (@protocol), effect and termination fences (@pure, @total), and dependent types with proofs (@proof) are all rungs — each a decorator or a type, each opt-in, each invisible to code that does not ask. Model checking (@spec) is the one piece that lives in an extension, and the split is deliberate: the theory of proof is decades old and belongs in the core, while the engine of a model checker is volatile and belongs behind the extension boundary.

The reasoning

Three of Makoto’s own rulers decide the shape.

The opt-in test (chapter 01) is the gatekeeper. A refinement, a proof, a protocol — none of them may leak onto the code of someone who does not use them. That is why each is summoned by a decorator or a type, never woven into the grammar everyone reads: a .mko that proves nothing looks exactly like one written before this layer existed. It is @supervisor all over again — sophistication that is there when you reach for it and gone when you do not.

Unify by concept (chapter 01) is why the layer added almost no new vocabulary. A refinement is a contract (@requires/@ensures, chapter 07) that travels with the type instead of the function, so it reuses the contract’s own way of naming a value — reference-by-type, or the named slot of a named return — rather than inventing a magic it. Ownership at the type level is the @transfer flow-analysis (chapter 02) lifted from the parameter to the decl. A proof is a program (Curry–Howard): a total recursive function whose match is the induction, so there is no theorem keyword and no tactic language in the core. dual is a type-operator because it produces a mirrored type, not a decorator, which only annotates. The layer grew by generalizing what was already there, not by bolting on a second system.

Honest names (chapter 12) settled the words. The academic terms are linear and affine; the decorators are @must_consume and @consume_once, because the reader of the code should learn the consequence from the name and meet the theory once, in the docs — and because they form a family with the existing @consume, so the whole memory-and-ownership realm speaks one dialect.

And the core-versus-extension call rests on the ruler from chapter 11 and section 20 of the design doc: the stable stays in the core, the volatile becomes an extension. Dependent type theory has been stable since the 1970s and runs in four production languages; it is core. A model checker’s engine — bounded search, state-explosion heuristics, external-tool bridges — turns over with the state of the art; it is an extension. The pre-1.0 freedom to grow the core is spent on what will still be true in twenty years, and withheld from what will not.

Why not the alternatives

• Why not Rust’s borrow checker? Because it is the anti-example the whole language is built against (chapter 00): a verification discipline that leaks into every signature, paid by everyone, always. Makoto keeps the guarantee (a resource used the right number of times) and pays for it only on the types that ask, because shared-nothing (chapter 04) makes the analysis local — no lifetimes to thread.
• Why not a separate proof language, or a .mkop file type? The first instinct was to isolate the proof tier behind its own file extension, the way the UI is isolated. But the UI earns a file type by volatility and a radically different grammar (markup); the proof tier is neither — it only adds to the type system, and its theory is stable. What actually needs isolating is not the syntax (a file boundary) but the soundness (a semantic fence): proofs are consistent only over a total, pure, strictly-positive fragment. That fence is @proof, opt-in by use — not a file everyone has to know exists.
• Why not Bend/Kind’s model — prove everything, run on a proof-native runtime? Because that is all-or-nothing at the top rung, and it pays the cost of the top rung everywhere. Makoto’s ladder lets a program prove the 5% that is critical, refine the next chunk, check the rest at runtime, and leave the bulk untouched — and the proved parts erase to ordinary functions with the indices gone, so there is no proof-runtime tax on the code that calls them.

The concrete pain

The index read that was “obviously in bounds” until the day it was not. The two channel endpoints that each sat waiting to receive, and the process that hung instead of crashing honestly. The transaction committed on one branch of an if and silently forgotten on the other. The comptime function that looped forever and took the compiler with it (a real bug the campaign found). The units error that flew a probe into a planet. Each is an obligation that no one had a place to state, so it went unchecked until it failed. The ladder’s job is to give every one of them a rung.

The mental model

A guarantee is an obligation on a predicate, and the compiler discharges it as high as it will go — unrepresentable if it can, proven if it must, checked if it cannot be proven, signed by you at the last. You climb the ladder one obligation at a time, and nothing you do not summon ever costs you.

The accepted friction

Proofs cost author time — the tedious term, the induction spelled out — and that cost is real; the bet (chapter 11’s, and the industry’s shift) is that author time on a critical kernel is cheaper than the incidents it prevents, and that the cost falls only on the fragment that summoned it. Two smaller frictions are named on purpose. @total becomes mandatory on any comptime function used in a type — a new obligation where before there was none — because an unsound proof is worse than no proof; it is the price of the kernel being trustworthy. And the ergonomic top of the layer — tactics, the @by block — is deliberately deferred to self-hosting, because doing it right needs the compiler’s own AST as a library, and with it come three permanent problems said out loud rather than discovered late: macro hygiene, the AST as a public contract, and error attribution through expansion. The layer ships without them, and is written so they wrap it later with no rework.

Back to the index