Will this program ever stop? One machine that can be any machine. And every interesting question about meaning.
Run it: ./selfie -c loop.c -m 1. It has not stopped yet. Will it?
You can reason: c is odd, adding 2 keeps it odd, and 0 is even — but the machine wraps at 264, so does c ever become 0? Odd plus even is odd, always, and wrapping preserves parity. It never stops.
You proved that. Could the compiler have? For this program, with effort, yes. For every program? That is today's question.
Suppose H(P, x) decides, for every program and input, whether P halts on x.
Build D(P): ask H whether P halts on P — then do the opposite. A call, a conditional, a loop, a return. All in C*.
Now run D(D). It halts exactly if it doesn't. Contradiction. So H never existed.
Turing, 1936 — the same paper that defined the universal machine, and thus invented the computer. The limit and the machine arrived together.
A machine used to be its job — to sort instead of add you built a different machine. Turing's move: put the machine's description on the tape, as data. Then one machine U reads any description and does whatever that machine would do.
That is universality: one piece of hardware, every possible behaviour, because the behaviour arrives as notation. Your phone is not phone-shaped. It is U holding a description.
Hand a decider its own description: contradiction, no H. Hand a machine any description: every program at once, one U. One sentence, read twice.
How long is the code? Does it parse? Does it use this library? Are the types consistent? Does it contain a loop?
Is it correct? Is it equivalent to that one? Does it ever divide by zero? Is it free of infinite loops? Is it safe?
So every practical tool — a type checker, a test suite, a linter, a model checker, a fuzzer, a proof assistant — is a deliberate approximation: sound but incomplete, or complete but unsound, or exact only within a bound. Choosing which to give up is the discipline.
A statute says no vehicles in the park. A car, plainly. And then the arguing starts: an ambulance, a bicycle, a memorial jeep. No redrafting removes the penumbra — only moves it. The words are finite; the situations are not.
So law stops trying to settle meaning in the text and builds an institution: courts, appeals, precedent. Not a workaround — the only available design. Rice's theorem, with no mathematics in it.
| year | who | the list | the diagonal object |
|---|---|---|---|
| 1891 | Cantor | all real numbers | a number on no row |
| 1901 | Russell | all sets | the set of non-self-members |
| 1931 | Gödel | all provable sentences | "I am unprovable" |
| 1936 | Tarski | all definable predicates | "I am false" |
| 1936 | Turing | all decidable questions | a program that defies its judge |
| 1953 | Rice | all semantic properties | all of the above, at once |
Assume a complete list. Ask each item about itself. Answer the opposite. Learn the move once and you own the century.
A machine, a method, or a person that settles all questions. No complete rulebook, no self-certifying system, no automatic correctness.
Mathematics is not a finished building but an open frontier; engineering is a craft rather than a lookup; and judgement — yours — never becomes redundant.
Beware of bugs in the above code; I have only proved it correct, not tried it.Donald E. Knuth, 1977
Systems: two ways to build an operating system, why they are the same, why virtualization is used anyway, and the loop at its centre — the kernel that needs what it provides.