Can a Math Proof Also Be a Computer Program?
The Day a Tiny Bug Blew Up a Rocket
On June 4, 1996, the Ariane 5 rocket rose into the sky, then suddenly pitched sideways and self-destructed. The culprit? A small computer program that tried to fit a 64-bit number into a 16-bit slot. No one saw it coming — because no human could realistically check every line of the code.
That disaster made people ask: is there a way to be absolutely certain that a program does what it’s supposed to? Around the same time, a quiet revolution was already happening in logic. A Swedish philosopher, Per Martin-Löf (born 1942), had created a new kind of mathematics — one where a mathematical proof isn’t just a chain of reasoning, but also a piece of code that you can run. He called it intuitionistic type theory, and it turned the age-old link between logic and computation into something airtight.
To see how, we need to rewind to two earlier breakthroughs: a mathematician who refused to trust infinity, and a philosopher who ran into a famous paradox.
Why Some Mathematicians Stopped Trusting Infinity
In the early twentieth century, the Dutch mathematician L.E.J. Brouwer (1881–1966) argued that some of the most common rules of logic were too sloppy for mathematics. In particular, he rejected the law of excluded middle — the idea that every statement is either true or false, even if we have no way of proving which one. Brouwer said that a mathematical claim is only true if we can actually build a proof-object for it, a construction that shows it directly.
His philosophy became known as intuitionism. It turned out that intuitionistic logic — a logic without the law of excluded middle — works very differently from the classical kind. For example, in classical logic you can prove that there exist two irrational numbers (a) and (b) such that (a^b) is rational, without knowing which pair works. In intuitionistic logic, you have to produce an actual example. Brouwer wanted math to be constructive.
Around the same time, the British philosopher Bertrand Russell (1872–1970) was dealing with a different threat: a paradox that could make the foundations of mathematics collapse. Russell showed that if you talk about “the set of all sets that do not contain themselves,” you end up with a contradiction. To fix this, he invented type theory, a system where every mathematical object belongs to a specific type — number, set of numbers, function from numbers to numbers, and so on — and you can’t treat things of different types as the same. This blocked the paradox by making the dangerous sentence ungrammatical in the language of types.
For decades, intuitionism and type theory were separate worlds. Then the computer age brought them together in an unexpected way.
The Moment Logic Met Programming
In the 1950s and 60s, logicians began to notice a strange pattern. The American mathematician Haskell Curry (1900–1982) saw that the structure of logical reasoning looked almost identical to the structure of a typed programming language. Then William Howard (working in 1969) extended the idea to predicate logic. The insight became known as the Curry-Howard correspondence, and it can be summed up like this:
A proposition is the type of its proofs.
What does that mean? Think of a type as a label that tells you what kind of thing something is. In a programming language, the type int means “integer,” and only numbers can have that type. Under the Curry-Howard lens, a logical statement like “it is raining” is itself a type — the type of all possible proofs that it is raining. A particular proof of that statement is an object (a piece of data) that belongs to that type. We write p : A to mean “p is a proof of proposition A.”
Different logical connectives turn into familiar type constructors:
- “A and B” becomes the product type A × B, whose elements are pairs ((proof_of_A, proof_of_B)).
- “A implies B” becomes the function type A → B, a function that converts any proof of A into a proof of B.
- “There exists an x such that P(x)” becomes a dependent pair type, where you produce a witness (a) together with a proof of (P(a)).
- “For all x, P(x)” becomes a dependent function type, a program that, given any input (a), returns a proof that (P(a)) holds.
Suddenly, a mathematical proof could be seen as a program that computes evidence. And if you can run the program, you can check the proof automatically. This is the engine at the heart of intuitionistic type theory.
Why Your Phone’s Code Needs a “Family of Types”
Martin-Löf took the Curry-Howard correspondence and supercharged it. Ordinary typed programming languages can say things like “this variable is an integer.” Martin-Löf’s system allows types to depend on values. This is called a dependent type, and it’s the secret that lets you express deep mathematical properties inside a computer.
Imagine you want to say, “the list (x) has length 3.” In a dependent type system, “list of length (n)” can be a type that depends on the number (n). A list with 3 items has type List A 3, a list with 0 items has type List A 0. If you write a function that expects a list of length exactly 3, the computer can verify at compile time that you never accidentally pass an empty list.
The same trick applies to numbers. In the theory, there is a type (\mathbb{N}) of natural numbers, constructed from zero and a successor operation, just as Peano arithmetic builds them. Using dependent types you can define the relation “(x < y)” not as a mere statement, but as a type whose elements are proofs (computations) that (x) really is less than (y). Proving the division theorem — “for any (m > 0), there exist (q) and (r) such that (m q + r = n) and (m > r)” — produces a proof-object that is literally a program: give it (m), (n), and a proof that (m>0), and it hands you back the quotient (q), the remainder (r), and proofs that the equation holds.
Because every piece of reasoning in this logic is a program, the logic is a functional programming language. And because the rules are designed carefully, every program that passes the type-checker is guaranteed to terminate. You can write a function that loops forever; the type system will reject it before it ever runs.
A Universe That Doesn’t Eat Itself
If propositions are types, then what is the type of all small types? Early on, Martin-Löf tried to include a type of all types, period. That turned out to be inconsistent: the French logician Jean-Yves Girard (born 1947) showed that it allowed a version of the Burali-Forti paradox, just as Russell’s set of all sets was explosive. So Martin-Löf introduced a universe of small types, called U. U contains types like (\mathbb{N}), (\mathbb{N} \to \mathbb{N}), lists of numbers, and so on. U itself, however, is not a member of U; it’s a “large” type that sits outside. This is similar to the way set theorists posit a Grothendieck universe — a box of sets closed under standard operations but not containing itself.
You can then build a whole tower of universes: (\mathbb{U}_0 : \mathbb{U}_1 : \mathbb{U}_2 : \cdots) . Each universe contains all smaller ones as elements. This keeps the system predicative: you build from the bottom up, never defining a type by referring to a collection that already includes it. Classical higher-order logic often does the opposite, defining sets impredicatively (e.g., “the least upper bound” by quantifying over all real numbers, including the one you’re defining). Intuitionistic type theory refuses to do that. It stays grounded, piece by piece.
So, How Do We Know the Rules Are Correct?
You might wonder: if this whole system is a formal language of types and programs, what guarantees that the rules themselves make sense? Martin-Löf didn’t rely on set theory, the usual meta-language of mathematics. Instead, he gave meaning explanations that are meant to be understood directly, without assuming any prior mathematical framework.
The key idea is that every type and term can be computed to a canonical form. A canonical form is a term whose outermost part is a constructor — something that tells you how it was built. For natural numbers, the canonical forms are 0 and s(a) (successor). For functions, it’s a lambda expression like λx.b. The meaning of a judgment like “(a) has type (A)” is then: if you compute (A) to a canonical type, and compute (a) to a canonical value of that canonical type, the result fits the expected shape.
For example, to say “there is a proof of (A)” (written (A) true) is to say you can produce some term (p) such that the judgment (p : A) holds — that is, you can run the proof. This is why proof-objects are sometimes called truth-makers. The meaning explanations are pre‑mathematical; they don’t invoke sets or large cardinals. They’re just rules about how computation works, and they justify all the inference rules of the theory.
Because the computation rules are simple and well-founded (no infinite descending chains of sleight‑of‑hand), the system is predicative and the equality of types and terms is decidable. That means a computer can check, fully automatically, whether a given program is well‑typed and whether two terms are equal. No human guesswork needed.
From a Philosopher’s Desk to the Code That Flies Your Plane
So why does this arcane logic matter to someone who just wants their phone not to crash?
Because Martin-Löf’s ideas became the foundation of several proof assistants: computer systems that help you write not just programs, but guaranteed‑correct programs. Two of the most prominent are Coq and Agda, both based directly on intuitionistic type theory. These tools have been used to prove major theorems — like the Four‑Color Theorem and the Feit‑Thompson Theorem — as well as to verify real‑world software. The French researcher Xavier Leroy used Coq to create a verified C compiler; you can compile a program, and the proof assistant ensures that the compiled machine code does exactly what the source code says, with no hidden errors.
In 2008, Georges Gonthier explained that his team’s formal proof of the Four‑Color Theorem worked by “to turn almost every mathematical concept into a data structure or a program in the Coq system,” so that the whole enterprise became one of program verification. This is exactly the Curry‑Howard vision: a proof is a program, and checking the proof is just type‑checking and running that program.
Today, type theory is also creeping into mainstream programming languages. Haskell’s advanced type features, for example, were inspired by dependent types. Slowly, the dream of software that cannot crash is becoming real — and it began with a philosopher who asked how we can know that a proof is truly airtight.
Think about it
- If every proof is a program, does that mean there are true statements that cannot be expressed as types? What would that say about the limits of logic?
- A computer can check a formal proof automatically. Does that make the proof more trustworthy than one a human mathematician writes by hand, or just differently trustworthy?
- If a self‑driving car’s software is checked by a proof assistant and declared bug‑free, would you feel completely safe riding in it? Why or why not?
