The crisis that built
your computer

In 1931, a 25-year-old named Kurt Gödel destroyed the first two items on the list with a single move so clever it still feels like a magic trick. Here's the whole thing in slow motion.

Start with an observation: arithmetic is expressive. It can talk about a lot. Gödel's first insight was that it can talk about itself — if you're willing to be sneaky. Every symbol in your formal system (0, +, =, the logical connectives, variables) gets assigned a number. A statement is a string of symbols, so it becomes a sequence of numbers, which you fold into one big number with a fixed recipe. A proof is a sequence of statements, so it too becomes a number. This is Gödel numbering, and the first widget lets you run the encoder yourself.

Once statements are numbers, statements about numbers are secretly statements about statements. The sentence "there is no number that encodes a valid proof of statement #N" is itself just an arithmetic claim about numbers — so it has its own Gödel number. You've smuggled provability into the language as a property of integers.

Now the diagonal trick — the same move Cantor used in Chapter 6 to out-count the integers, the one that's going to show up three times in this chapter. Gödel uses it to build a self-referential sentence. Call it G:

Now run the two cases, the way you'd trace a suspicious branch:

• Suppose the system can prove G. Then G — which asserts it has no proof — is false. A system that proves false things is broken (inconsistent). Throw it out.
• Suppose the system can't prove G. Then what G says is exactly true: it has no proof. So G is a true statement the system cannot reach.

For any consistent system rich enough to do basic arithmetic, the second case is the one you're stuck with. There is a true sentence sitting just outside its reach — and you can't patch it by adding G as a new axiom, because the trick just builds you a fresh G′ for the bigger system. This is Gödel's first incompleteness theorem. Completeness: dead. The dream of an axiom set that proves every truth is provably unbuildable.

The second theorem is the gut-punch. Among the true-but-unprovable statements is the sentence that asserts "this system is consistent." A system can't prove its own consistency from the inside — not unless it's already inconsistent, in which case it can prove anything and the proof is worthless. Hilbert wanted a safe, internal certificate of consistency. Gödel proved that certificate can never be issued. Item two: dead.

No theorem in history has been more abused at dinner parties. Gödel gets dragged in to justify everything from "science can't know anything" to "therefore, God." So before we go further, the guardrails — because the actual result is precise, and the precision is the whole point.

It does not mean math is broken. Nothing collapsed. Arithmetic still works; your bank balance is fine. The theorems say a specific formal system can't prove certain true things about itself from inside. That's a statement about the reach of a fixed proof-machine, not about whether math is reliable.

It does not mean "everything is relative" or "truth is subjective." The opposite, really — Gödel's G is objectively true. The result depends on there being a sharp fact of the matter about what's true. It limits provability-from-inside, not truth.

It is not a license for mysticism. "Gödel proved the mind transcends machines / the universe is unknowable / my crystals work" — no. The theorem has hypotheses, and they're narrow: the system must be consistent, and it must be rich enough to encode arithmetic. Plenty of useful formal systems dodge it entirely. The theory of real numbers as a geometric field is complete and decidable. So is Presburger arithmetic (addition, no multiplication). The incompleteness only bites once you have enough machinery to build self-reference — which, it turns out, is not much.

Two items down. One left: decidability. Is there a mechanical procedure that decides any statement? To even attack the question, somebody had to answer a more basic one that nobody had ever pinned down: what is a mechanical procedure? What does it mean to "compute" something? In 1936, two people answered, separately, from totally different directions.

Alan Turing's answer was a machine. Imagine the dumbest possible computer you can still describe precisely. It has an infinite paper tape divided into cells, each holding a symbol. A head sits over one cell and can read it, write a new symbol, and shuffle one step left or right. The machine has a handful of internal states, and a lookup table: given (current state, symbol under the head), the table says what to write, which way to move, and which state to go to next. That's the entire machine. No arithmetic unit, no memory hierarchy, no clever instructions — just a head crawling along a tape following a tiny rulebook. Turing's claim: anything a human computer could do by following rote rules, this machine can do too. The second widget is one of these machines. Run it.

Alonzo Church's answer was a notation. No machine, no tape — just functions. You start with variables and exactly one construction: λx. (body), an anonymous function of x. You build everything — numbers, booleans, pairs, recursion, all of it — by nesting and applying these lambdas, and the only rule is substitution: applying a function means plugging the argument in for the variable. This is the lambda calculus, and if it smells like the core of every functional language you've ever written, that's because it is the core. Scala's a => body is Church's λa. body wearing a hat.

A machine crawling a tape. A grammar of nested functions. They could not look more different. And yet — they define the exact same class of computable functions. Anything one can compute, so can the other. Add in Gödel's own "recursive functions," and Post's tag systems, and every other honest attempt anyone has made since: same class, every time.

Now we have a precise "computable," so we can finally ask Hilbert's third question as a real math problem — and answer it. Turing picked a specific job and asked whether any program could do it: given a program and its input, decide whether it eventually halts or runs forever. Call the hoped-for decider halts(P, x) — returns true if program P halts on input x, false if it loops. A perfect static analyzer. Every engineer wants this.

It can't exist. And the proof is the diagonal trick a third time — Cantor in Chapter 6, then Gödel two sections ago, now Turing. Watch the detonation. Suppose halts exists. Then I can write this little troublemaker:

Now the lethal question: does trouble halt when you feed it to itself? Trace it.

• If trouble(trouble) halts, then by definition halts(trouble, trouble) returned true — so trouble took the while(true) branch and loops forever. It doesn't halt.
• If trouble(trouble) loops, then halts returned false — so trouble took the return branch and halts immediately.

It halts if and only if it doesn't. A flat contradiction, same flavor as Gödel's G and Cantor's missing diagonal number. The assumption was the bug: no general halts can exist. Hilbert's decidability dream — an algorithm that decides any statement — dies right here, because deciding provability would let you decide halting. All three items: dead. The whole spec, rejected.

This isn't an engineering gap that a smarter team will close next quarter. It's a proof of impossibility, permanent. And it generalizes brutally. Rice's theorem says that every non-trivial question about what a program does — does it ever output 42? does it leak memory? is it equivalent to this other program? — is undecidable in general. Static analysis has a ceiling, forever. Your linter is heuristics all the way down, and it has to be. That's not laziness; it's a theorem.

Back up to the paradox that started all this. Russell didn't just point at the crack — he proposed a fix, decades before Gödel. His paradox came from a set being allowed to contain itself, mixing levels that should never touch. So Russell stacked everything into a hierarchy of types: basic objects at level 0, sets of objects at level 1, sets of those at level 2, and a hard rule — a thing can only contain things of a strictly lower level. "The set of all sets that don't contain themselves" is now a grammar error. It doesn't typecheck. The paradox can't even be written down.

Sit with that, because it's the move your compiler makes every single day. You can't form the bad expression — not because it's false, but because it's ill-typed. The error happens before the question is even askable.

For a long time types were a defensive patch — a fence around the paradox. Then in 1972, Per Martin-Löf turned the fence into a foundation. His intuitionistic type theory rebuilds all of mathematics on types: a number is a type, a function is a type, a proposition is a type, even "these two things are equal" is a type. No separate logic bolted on top — the logic is the type system. It's the lineage behind today's proof assistants, the ones we'll watch check real theorems in Chapter 13.

And here's the bargain at the heart of it — the same bargain you accept every time you reach for Scala over a dynamic language: you restrict what you're allowed to write, and in exchange you get a machine-checkable guarantee. Give up the freedom to mix levels, to call a function on the wrong thing, to forget a case — and the machine hands you a proof that whole classes of nonsense can't occur. Sound familiar? That's not an analogy to your compiler. As the next section shows, it's literally the same thing.

Now the punchline the whole chapter has been walking toward. In the 1930s–60s, Haskell Curry and William Howard noticed that two things mathematicians thought were unrelated — formal logic and typed programming — are the exact same structure, just with different vocabulary. This is the Curry–Howard correspondence, and once you see it you can't unsee it.

The dictionary is short and shocking:

• A proposition (a thing that might be true) is a type.
• A proof of that proposition is a program (a value) of that type.
• Implication A ⟹ B is the function type A => B — a recipe turning evidence for A into evidence for B.
• "And" is a pair (A, B); "or" is a sum Either[A, B].
• Chaining implications — proving A⟹B and B⟹C to get A⟹C — is just composing functions.

So "proving a theorem" and "writing a program with a given type" are the same activity. To prove a proposition, you inhabit its type — you exhibit a value of it. If the type is empty (no possible value), the proposition is false, unprovable. The compiler that checks your types is, secretly, a proof checker. The third widget is the Rosetta stone — pick a proposition and watch it appear three ways: as plain logic, as a Scala type with a one-line proof, and as Haskell.

Hold this thought for the finale. If a proof is just a program of the right type, then a machine can check a proof by type-checking it — no human refereeing required. Chapter 13 industrializes exactly this idea: entire research papers, written as programs, verified by a compiler. The toy below is the seed of that whole enterprise.

Let's make Curry–Howard concrete with a real theorem: if A or B holds, then B or A holds — commutativity of "or." Its type is Either[A, B] => Either[B, A]. To prove the theorem, write a total function of that type. The pattern-match exhaustiveness check is the proof checker: cover both cases and the compiler signs off; forget one and it warns you your proof is incomplete.

Hilbert asked for a guarantee and got three impossibility proofs. But look at the wreckage. To prove decidability impossible, Turing had to invent a precise model of computation — and the stored-program computer, the thing on your desk, is a Turing machine with a budget. To answer "what is computation," Church built the lambda calculus — which became Lisp, then ML, then the Haskell and Scala you write today; every functional language is Church's notation industrialized. Russell's types grew into the type systems that catch your bugs at compile time. And Curry–Howard fused logic and programming so tightly that proof assistants can now verify mathematics by type-checking it.

A crisis about the limits of truth handed us the limits of machines — and, almost as a side effect, the machines themselves. The logicians went looking for certainty and accidentally invented computer science. Not a bad failure.