Halting problem

Why can no program be written that reliably predicts whether another program will ever finish?

It sounds like a hard engineering problem rather than an impossible one. Programs are finite texts, and their behaviour follows mechanically from their instructions. Surely a careful enough analyser, given a program and its input, could work out whether it eventually stops.

Yet the answer is not "nobody has managed it yet". It is that nobody can, ever, whatever hardware or cleverness is brought. Before believing so strange a claim, we should ask what exactly is being ruled out — because the sweeping version of the statement is not the true one.

First, narrow it honestly. Plenty of programs are trivial to judge: a loop counting to ten halts, while true do nothing does not. The claim is about one procedure that, for every program and every input, always terminates itself and always answers correctly. Three demands at once. Drop any one and the task becomes possible — worth holding onto, because that is where all the practical work happens later.

Second, why not simply run it and see? You can, and it is instructive what that buys. If the program halts, you find out eventually. If it has not halted yet, you have learned nothing — you cannot distinguish "will not halt" from "has not halted yet". So halting is recognisable but not decidable, and the missing side is the whole difficulty.

Could we cap the wait — if it has not stopped in N steps, declare it never will? Only if N could be computed from the program. It cannot, and the busy beaver function shows why with unnerving concreteness. Among five-state, two-symbol Turing machines, the longest-running one that eventually halts runs 47,176,870 steps; that value was settled by a collaborative machine-verified proof in 2024, and I am recalling it rather than deriving it. The six-state value is unknown and understood to be beyond astronomical. Busy beaver grows faster than any computable function, so no computable bound is ever safe.

Now the argument itself, which is short. Suppose the decider exists — call it Decider, taking a program and an input, always terminating, always right. Then anyone holding it can write Contrary: given a program P, ask Decider whether P halts when run on its own text. If it says P halts, loop forever. If it says P runs forever, stop immediately.

Run Contrary on Contrary. If Decider says it halts, Contrary loops, so Decider was wrong. If Decider says it loops, Contrary stops, so Decider was wrong. There is no third case, and the assumption that produced the contradiction was the decider's existence. Notice what the argument did not need: nothing about speed, memory, technique or intelligence. Only that Contrary can be built — and a program that calls another and does the opposite of what it says is entirely ordinary code.

Let us try to break the result rather than admire it. Is the trick just that Contrary is perversely self-referential, so a decider might still work on the sensible programs people write? Rice's theorem, from 1953, closes that escape: every non-trivial property of what a program computes — whether it ever outputs a given value, whether it matches some other program, whether it touches a given address — is undecidable by essentially the same reduction. Self-reference is not a curiosity smuggled in; it is unavoidable in any system expressive enough to run arbitrary programs.

Here is the objection that actually lands. Real computers are finite. A machine with n bits of state has two-to-the-n configurations, so it must halt or repeat one within that many steps, and repetition means it never halts. For real hardware, halting is decidable. Yet the escape is worthless: for even a few gigabytes of memory, two-to-the-n dwarfs anything physical. Undecidability and intractability are different claims, routinely merged, and the honest position is that the finite argument defeats the theorem and changes nothing.

The most useful correction is about what the theorem permits. It forbids a universal decider that is always correct and always answers. It says nothing against a tool that is always correct but sometimes answers "I cannot tell" — which is exactly what real termination provers do, discharging the great majority of loops and flagging the rest for a human. It says nothing against restricting the language: total functional languages, and the structural-recursion checks in proof assistants, guarantee termination by refusing to express programs that might not terminate. And it says nothing against being right on the programs anybody actually writes. Undecidable does not mean unanalysable; it means no single method covers everything.

It is also worth seeing how this sits beside Gödel's incompleteness, since the two are the same self-reference in different clothing. Gödel builds a sentence asserting its own unprovability; Turing builds a program consulting a predictor and doing the opposite. And one yields the other: if some consistent, mechanically checkable system proved every true statement of the form "this program never halts", you could decide halting by enumerating proofs while running the program, taking whichever finished first. Since halting is undecidable, no such system exists — incompleteness, reached from computation.

Two misreadings are worth naming as wrong. The theorem does not say human beings cannot tell whether a program halts; it constrains algorithms, and whether that constrains us depends on whether our reasoning is itself algorithmic, which the theorem does not settle and which remains contested. Nor is it a claim that the analysis is merely very hard — the decider's own existence is what makes the counterexample constructible, so any improvement to it improves the thing that defeats it.

• Why proof assistants accept a language in which some computations cannot be written, and what is lost.

Every term the collection defines is gathered in the glossary.