Here is a piece of software everyone would pay for: a perfect bug-checker. You feed it any program together with any input, and it tells you — reliably, in finite time — whether that program will eventually finish or spin forever in an infinite loop. No more hung servers, no more frozen apps. Surely, with enough cleverness, someone could write it?
No. And this isn't a "we haven't managed it yet" — it is a theorem. In 1936 Alan Turing proved that no algorithm can decide, for every program-and-input pair, whether it halts. The universal bug-checker is not merely hard to build; it is mathematically impossible. This page is about that boundary — the line between problems a machine can settle and problems no machine ever can — and about the beautiful self-referential trick that proves the line is real.
A decision problem is a yes/no question posed about an input: "Is
The two words are everything:
Undecidable is a statement about the problem, not about us. It says the set of correct yes/no answers is so tangled that no finite mechanical procedure can reproduce it.
Notice what is not being claimed. For particular programs you can often see the
answer at a glance — a program with no loops obviously halts; a bare while (true) {}
obviously does not. The theorem is about a single algorithm that must handle
all programs at once. That one universal decider is what cannot exist.
Line the programs up as rows and their possible inputs as columns; cell
The proof is a proof by contradiction driven by self-reference. We assume the impossible tool exists and then build a program that jams it.
The self-reference — a program reasoning about a program reasoning about itself — is exactly
Cantor's
Here is the troublemaker as illustrative — and deliberately un-runnable — TypeScript. It cannot
actually run, precisely because the
The whole proof lives in that one if: whatever halts predicts about
Between "solvable" and "hopeless" sits a crucial middle rung. A problem is semi-decidable (equivalently recursively enumerable, r.e.) when there is an algorithm that halts and says "yes" on every yes-instance, but on a no-instance is allowed to run forever. You get a guaranteed yes; you never get a guaranteed no.
The halting problem itself is semi-decidable: to check whether
Turing did not build his machine to check software — he built it to answer a question in
logic. In 1928 Hilbert and Ackermann posed the
Entscheidungsproblem ("decision problem"): is there an algorithm that, given any
sentence of
In 1936 Church and Turing answered: no — first-order validity is undecidable. There is no mechanical procedure that always terminates with a correct valid/not-valid verdict. This is where the halting problem and pure logic meet: Turing reduced HALT to validity, so a validity-decider would give a halting-decider, which we just proved cannot exist.
But — and this is the elegant consolation — first-order validity is semi-decidable. By Gödel's completeness theorem, a formula is valid if and only if it has a formal proof, and proofs are finite objects you can enumerate systematically. So a proof search that grinds through every candidate derivation will find a proof of any valid formula and halt saying "valid". Fed an invalid formula, though, it may search forever, never certain none exists. Validity is recognisable but not decidable — exactly the semi-decidable middle rung.
The single most common misreading: hearing "undecidable" as "really difficult" or "nobody has found the algorithm yet". Both are wrong. Undecidable is a proven impossibility — a theorem that no algorithm can ever exist, however much compute, cleverness, or time you throw at it. It is not a challenge awaiting a genius; it is a closed door with a proof nailed to it.
And do not blur semi-decidable with decidable. Being able to confirm every "yes" is not the same as being able to settle every case. The halting problem and first-order validity are both semi-decidable and both undecidable at the same time — you can recognise the yes-instances, yet no procedure resolves every instance with a guaranteed answer.
It doesn't — not perfectly. Real tools sidestep the theorem by being conservative: they answer only "definitely halts", "definitely loops", or a humble "I'm not sure". A linter that flags some infinite loops while missing others, or occasionally cries wolf on safe code, breaks no law — it simply never claims to be the perfect universal decider. Type checkers, termination analysers, and model checkers all live in this pragmatic world: correct when they commit, silent when they can't. The impossibility is only of a tool that is always right on every program. Approximate, one-sided, or "usually right" tools are alive and well — and are why your IDE can still be useful.