Types as Propositions: Making Wrong Programs Unwritable

The previous lesson wrote a program, wrote a specification alongside it, and proved they agree. There is a second approach that removes the gap by construction.

Rather than checking a program against a separate spec, encode the specification in the type, so strongly that no incorrect program can be given that type. Correctness then follows from type checking, which every compiler already does.

The familiar version of this idea is already in ordinary languages. A function typed as taking an integer cannot be handed a string, and no proof is needed because the program does not compile. The type made a class of errors unwritable rather than detectable.

The question is how far that goes. Ordinary type systems catch shape errors and stop well short of behaviour: nothing in List -> Int says the result is the list's length rather than its first element or 42.

What follows is the machinery for pushing that boundary until the type says exactly what the function must do.

The foundation is an observation that looks like a coincidence and is a deep structural identity, known as the Curry-Howard correspondence.

Read a type as a logical proposition, and a program of that type as a proof of it.

Check the first row against intuition. A function from A to B converts any A into a B, which is exactly what a proof that A implies B does: given evidence for A, it produces evidence for B. Function composition is transitivity of implication.

The row that carries the most weight is the fourth. A proposition is false exactly when its type has no values, because there is nothing that could serve as evidence.

So proving a theorem and writing a program are the same activity viewed from two directions, and a type checker verifying a program is a proof checker verifying a proof. That is not an analogy used for teaching; it is why proof assistants are built as programming languages.

Ordinary types are built from other types. List Int mentions a type. To express a specification, a type must be able to mention a value.

A dependent type is one that depends on a value. The canonical example is a list carrying its length: Vec Int 5 is a vector of exactly five integers, and 5 is a value appearing in a type.

That single capability changes what a signature can promise.

append : Vec A n -> Vec A m -> Vec A (n + m)
head   : Vec A (n + 1) -> A

The first says appending produces a vector whose length is the sum of the inputs' lengths. A wrong implementation, returning the first argument, does not type check: its length is n, and n is not n + m.

The second is the more striking one. Its argument type is a vector of length at least one, so head cannot be called on an empty vector. There is no runtime check, no exception, and no error case, because the situation is unrepresentable.

That is the pattern in general. A dependent type turns a runtime precondition into a compile-time obligation on the caller.

The four branches are the same property enforced at four different times, and the cost moves earlier as you go down.

Runtime checking is cheapest to write and discovers the problem at the worst moment. Testing moves discovery to development and covers only sampled inputs. Proof, from the previous lesson, covers all inputs but produces a separate artefact that must be maintained alongside the code.

The last branch collapses the artefact into the program. There is no separate proof to drift out of date, because the type is the specification and the implementation is the proof. They cannot disagree, since a disagreement is a type error.

That elimination of drift is the strongest argument for the approach. In the previous lesson's style, a proof and its program are two documents that must be kept consistent by discipline. Here consistency is what compilation means.

The correspondence demands something uncomfortable, and the reason is worth following because it is not arbitrary.

If a program of type T is a proof of proposition T, then a non-terminating program is a problem. Consider a function that loops forever while claiming to return a value of any type. It has the type, so it is a proof, and it proves everything, including False.

A logic that proves False is worthless. So the correspondence only holds if every program terminates.

That is why proof assistants such as Coq, Agda and Lean require termination, usually by demanding structural recursion on an argument that provably shrinks. Their core languages are total, and as the lesson What Undecidability Costs Real Tools sets out, that is the deliberate exit from Rice's theorem: the undecidability results assume a language that can express arbitrary computation, so a total language escapes them by giving up that expressiveness.

The practical cost is real. Algorithms whose termination is genuine but not structurally obvious must be restructured, or accompanied by a hand-written proof that a measure decreases. Writing a correct program the checker rejects is a routine experience, and it is the price of the guarantee rather than a defect.

The technique that makes dependent types practical is to attach evidence to values, so that constructing the value requires establishing the property.

A sorted list is not a list plus a separate claim of sortedness. It is a structure whose constructor demands a proof that the new element is in order.

data Sorted : List Int -> Type where
  Empty  : Sorted []
  Single : (x : Int) -> Sorted [x]
  Cons   : (x : Int) -> (rest : List Int)
           -> LessEq x (head rest)      -- evidence, required to build
           -> Sorted rest
           -> Sorted (x :: rest)

A value of type Sorted xs cannot exist unless every adjacent pair was justified, so a function accepting one may assume sortedness without checking. The assumption is discharged by whoever constructed the value.

This generalises into the standard idiom for the style. Rather than validating at every use, make the type constructible only in valid states, and validate once at the boundary where untrusted data enters.

The same idea appears in weaker form in ordinary languages, as newtypes and smart constructors: a ValidatedEmail type whose constructor is private and only reachable through a checking function gives a diluted version of the guarantee with none of the machinery.

Full dependent types are a research-adjacent tool, and the ideas have diffused far beyond the languages that implement them fully. That diffusion is where most engineers actually meet this.

Ownership and lifetimes. Rust's borrow checker is a type-level argument that no reference outlives what it points to and that mutation is exclusive. It is not general dependent typing, and it eliminates a whole class of memory errors at compile time by the same logic: make the bad program unrepresentable.

Typestate. Encoding an object's state in its type, so a closed connection has no send method, moves protocol errors from runtime to compile time.

Phantom types and units. Tagging a numeric type with its unit makes adding metres to seconds a type error, at zero runtime cost.

Exhaustive matching. Requiring every case of a sum type to be handled is a small dependent-typing idea in everyday use, and it is why adding a variant produces a list of every site needing attention.

The transferable instruction is the general one: when a property matters, ask whether it can be made unrepresentable rather than checked. That question is available in any language with a type system, and it does not require a proof assistant.

The fourth row is the fundamental trade. Hoare-style verification applies to code in the language you already use, at the cost of maintaining a second artefact. Type-level encoding removes the second artefact, at the cost of a language that will not accept some correct programs.

Neither dominates, and serious systems use both: dependent types for the core where the invariants live, and separate proofs for imperative code that a total language cannot express naturally.

Both traditions share a limitation the next lesson attacks. Each needs a human to state the invariant or design the type, so effort scales with the code being verified. The third tradition asks a different question: can correctness be checked exhaustively, by machine, with no invariant supplied at all?