The proof budget

I once spent an afternoon teaching TypeScript that a command list was non-empty. The helper worked, the red underline vanished, and the next function read untrusted JSON through as Config. I had proved a fact about the safe end of the pipe while leaving the input boundary open with a crowbar. Why was I proving the middle while a cast had kicked the front door off its hinges?

The plug gauge in the photograph checks one dimension ruthlessly and ignores everything it was never built to measure. Types work the same way: they can prove whatever their logic can state and their checker can verify, under the assumptions you supply. In practice, teams stop much earlier because specifications take time, requirements move, and a perfect proof of the wrong property still ships the bug.

The arrow already means implication#

Lean's propositions-and-proofs guide makes the connection literal. A value of type A can be evidence for proposition A, while a function A → B turns evidence for A into evidence for B. The kernel checks the resulting proof term.

variable {A B C : Prop}theorem compose    (ab : A → B)    (bc : B → C) :    A → C :=  fun a => bc (ab a)

type Fn<A, B> = (value: A) => B;const compose =  <A, B, C>(bc: Fn<B, C>, ab: Fn<A, B>): Fn<A, C> =>  (a) => bc(ab(a));

Both snippets prove the joint: given the first two arrows, an A → C can be built. Lean reads the letters as propositions when they live in Prop. TypeScript's structural type system treats them as sets of values accepted at each call site. Composition is proof composition when the types carry facts you care about. With ordinary application types, it usually proves that one output can be passed to the next input.

TypeScript checks a weaker claim. A function may throw, loop forever, mutate shared state, or forge a return value through any. Even an honest Email → Receipt cannot establish that a person read the message. The business nouns make a call signature sound more worldly than the guarantee the checker actually provides.

The ladder runs sideways#

“Most advanced” suggests one ranking, and these languages refuse to line up. Each picks a different balance among proof expressiveness, automation, executable code, kernel size, and daily ergonomics.

Liquid Haskell deliberately restricts its refinements to logic that fast SMT solvers can handle. Idris 2 can put a vector's length in its type and use Fin n to rule out an invalid index. F* combines richer types with automated verification for security-sensitive programs, while Lean and Rocq are comfortable when the theorem itself becomes the main artifact.

You pay for those choices in termination and proof search. Agda checks recursive definitions for termination, and Rocq restricts recursive constructions so a looping term cannot masquerade as evidence for any proposition. As the logic becomes richer, the checker usually asks for more guidance.

I learned that distinction while encoding a small state machine in Idris. The legal transitions felt good in the editor until one helper needed a proof that it preserved a length index and consumed the evening. I eventually moved the helper behind a tested runtime boundary because its proof changed more often than the bug it prevented. I still like the type, though I no longer treat difficulty as evidence of value.

Spend proof where failure compounds#

A proof pays best at a stable boundary used by many callers. Array bounds, protocol order, ownership, capability restrictions, serialization round trips, and cryptographic invariants qualify because one checked fact removes repeated defensive work downstream. A proof earns its keep when many callers get to stop checking the same fact.

Product copy, recommendation quality, whether checkout feels confusing, and what a remote service actually did resist the same treatment. You can formalize a model of them, but then the expensive question moves to whether the model matches the next release. I have not found a universal cutoff. I look for a costly failure, a stable statement, and enough reuse to amortize the proof.

Every theorem still relies on a trusted base: the kernel, chosen axioms, the compiler or extraction path, and whatever connects the model to the machine. F* can verify that code respects a protocol model. A foreign function can violate an assumption the proof accepted.

On the branch I kept, decodeConfig returns a validated configuration and the retry layer refuses the raw version. The payment call still checks the provider response at runtime and records the idempotency key beside it. I left that assertion in place because our code cannot inspect the bank's ledger.