1936 United Kingdom undecidable

On Computable Numbers

Alan Turing, 1936 — there is no general procedure to decide whether an arbitrary program halts. The first wall any solver hits.

Alan Turing, working at Cambridge and soon to leave for Princeton, defined a universal computing machine and proved that the Halting Problem — given a program and an input, decide whether the program eventually stops — has no algorithmic solution. The proof is a diagonal argument: assume a halting decider exists, construct a program that consults the decider on itself and does the opposite, and contradiction follows. The result predates electronic computers. It is the foundational impossibility result of computer science, and the ceiling above which no software-verification tool, no AI system, no formal method can ever rise. Every later impossibility result in this book — Rice 1953, the NP-completeness barrier, the limits of static analysis — descends from this one paper.

In plain terms

Imagine a tool that reads any program you hand it and answers, before running it, whether the program will eventually finish or run forever. Such a tool would be the answer to most questions in software. You could check, in advance, whether your code will hang. You could check whether a regression in the new version preserves the old behavior. You could check whether a refactor is safe. Turing proved, in 1936, that this tool cannot exist. Not "we have not built it yet." Not "it is too slow." Cannot exist, mathematically, ever. The proof is short and brutal. Suppose the tool exists. Call it Halts. Build a new program, Liar, that asks Halts what Liar itself will do — and then does the opposite. If Halts says Liar halts, Liar runs forever. If Halts says Liar runs forever, Liar halts immediately. Either way Halts has lied about Liar. But Halts was supposed to be always correct. Contradiction. No such tool exists. This is the ceiling. Every later result in this book — Rice's theorem, the undecidability of program equivalence, the NP-hardness of every interesting maintenance problem — sits underneath this 1936 proof. When you read in chapter four that you cannot, in general, decide whether a refactor preserves behavior, you are reading a corollary of this paper. When you read in chapter sixteen that AI cannot prove its own output correct, you are reading the same corollary. The first wall. No solver crosses it.