The Halting Problem

Symptom

Your CI has a test that hangs. Not fails — hangs. Somebody suggests the obvious fix: before running a test, check whether it terminates, and skip it if not.

Or: you are writing a plugin system, and you would like to reject plugins that contain infinite loops before you load them, because an infinite loop in a plugin takes down the host.

Or the version that gets funded: a static analyzer that flags every unbounded loop in a codebase, with no false positives and no false negatives, so the security team can finally close the “unbounded resource consumption” ticket class permanently.

Every one of these is a request for the same program, and that program does not exist. Not “is hard to write.” Does not exist, in the way that a largest prime does not exist.

Statement

There is no program $H$ that takes an arbitrary program $P$ and input $x$ and always correctly answers whether $P$ halts on $x$.

Three words carry the weight. Arbitrary: $H$ must work for every $P$, not for the ones you have. Always: $H$ must itself terminate with an answer, so “simulate it and see” is not a solution — it never returns on the inputs you most wanted to know about. Correctly: no wrong answers, ever.

The gap between recognizable and decidable is the whole content of the theorem, and it is exactly the gap between a debugger and an oracle. You can always confirm halting by waiting. What you cannot do is confirm non-halting.

Argument

Suppose, for contradiction, that $H$ exists: a program where H(P, x) returns true if $P$ halts on $x$ and false otherwise, always terminating.

Then write this, which is nine lines and does nothing clever:

def D(P):
    if H(P, P):      # does P halt when fed its own source?
        while True:  # ... then loop forever
            pass
    else:
        return       # ... otherwise halt immediately

D is a perfectly ordinary program: it calls a function we assumed exists, and branches. If $H$ is a program, so is D.

Now ask the only question available. What does D(D) do?

Case 1: D(D) halts. Then H(D, D) returned true, by the correctness of $H$. But look at the code: when H(P, P) is true, D enters while True and never halts. So D(D) does not halt. Contradiction.

Case 2: D(D) does not halt. Then H(D, D) returned false. But when H(P, P) is false, D returns immediately. So D(D) halts. Contradiction.

Both cases are impossible, and one of them must hold, since a program either halts or does not. The only assumption we made was that $H$ exists. So $H$ does not exist. $\blacksquare$

Where the diagonal went. This is T002 with the rows relabelled. Imagine the infinite table whose rows are programs $P_1, P_2, \dots$ (countably many, since programs are finite strings), whose columns are inputs in the same enumeration, and whose cell $(i, j)$ records whether $P_i$ halts on $P_j$. D is built to walk the diagonal and disagree with it: D behaves, on input $P_n$, in the opposite way to how $P_n$ behaves on $P_n$. So D differs from every row of the table in at least one cell, and therefore is not any $P_n$. But D is a program, and every program is a row. The only escape is that the table cannot be filled in — that $H$, the thing that computes the cells, is not a program.

Cantor concluded “the list is incomplete.” Turing arranged matters so the list must be complete — programs really are all enumerable — and therefore the contradiction lands somewhere else, on the halting oracle. Same flip, harder conclusion, and this is why it is worth reading the two proofs together.

The self-application is not the trick. Feeding D its own source looks like the sleight of hand, and it is the step people distrust. It should not be distrusted: passing a program its own text is something you do routinely, every time you run a compiler on its own source, and a quine is a fifty-character demonstration that self-reference needs no special power. The recursion theorem (T014) makes this exact: any program can be written to have access to its own source, with no loss of generality. The diagonal is not exploiting a loophole in what programs may do. It is using an ordinary capability at an inconvenient moment.

Forbids

The universal termination checker. No tool, in any language, at any budget, now or later, decides termination for arbitrary input programs. This is not a statement about current technology.

Perfect infinite-loop detection in a plugin sandbox. Which is why every real sandbox uses a timeout or a fuel counter instead — an answer to a different, decidable question (“does it halt within $n$ steps?”).

A sound, complete, terminating analysis for any property that encodes halting. And an enormous number of properties do, by reduction: dead code elimination, “is this variable ever used”, “can this pointer be null here”, “does this regex ever match”. Show that solving your property would let you solve halting, and your property inherits the impossibility. That machinery, reductions, gets its own post (T017); the generalization that every nontrivial semantic property falls this way is Rice’s theorem (T011), and it is the next one.

The mathematician’s version. Hilbert’s Entscheidungsproblem — a procedure to decide the truth of any first-order statement — dies here too, since a machine’s halting can be encoded as such a statement. Turing’s paper is titled after that problem, not after halting. Halting was the lemma.

Does not forbid

It does not forbid termination checkers, and this is the misreading with the highest cost. “Halting is undecidable” gets used, in real code review, to reject termination analysis as a category error. Meanwhile Coq, Agda, Lean, and Idris all ship termination checkers that work, are sound, and always terminate; Rust’s borrow checker and the Linux kernel’s eBPF verifier both require proof of termination before accepting code, and the eBPF verifier is in production on essentially every large fleet in the world. The resolution: these tools are allowed to say no to programs that in fact halt. A checker that answers {halts, don’t know} is trivially possible, useful, and totally different from what the theorem forbids. The theorem kills the checker with two exact answers, not the checker with a conservative one.

It does not forbid deciding halting for restricted languages. Every loop-free program halts, decidably. So does every program in a total language, every primitive recursive function, every terminating rewrite system, every SQL query without recursive CTEs, and every Dhall or Starlark configuration. This is the main reason configuration languages are not Turing-complete on purpose. If your inputs are not arbitrary programs, the theorem simply does not apply to you, and “but halting is undecidable” is not a valid objection to a language design that has already dodged it.

It does not forbid deciding halting for the program in front of you. The theorem quantifies over all programs; it is silent about any particular one. while (true) {} provably does not halt and the proof takes one line. The Collatz iteration is unknown, but “unknown” is a fact about mathematics in 2026, not a consequence of Turing’s theorem. Undecidability of the general problem is compatible with every specific instance you will ever meet being settled.

It does not mean “you cannot know if your program has bugs.” This is the pub version and it is false in a way that discourages useful work. Bounded model checking, exhaustive testing over a finite state space, TLA+ on a fixed configuration, and a type checker rejecting a null dereference all establish real facts about real programs. Undecidability constrains what a single algorithm can do uniformly over all inputs. It places no bound at all on what you can learn about one system.

It does not imply human minds exceed machines. The Lucas–Penrose argument says: a machine cannot decide halting, but I can see that while(true){} loops, therefore mind is not machine. The step is invalid. Humans do not decide halting either — nobody has settled Collatz — and the theorem is not about who is clever enough. It says no uniform total procedure exists, and that applies to any procedure a human could follow just as it applies to silicon.

Boundary

The result is sharp, so the interesting question is what sits immediately outside it.

• Bounded halting is decidable, and this is what everyone actually ships. “Does $P$ halt within $10^9$ steps?” is answered by running it for $10^9$ steps. Every timeout, watchdog, query governor, and eBPF instruction limit is this decision procedure. The cost is that you have replaced a question about the program with a question about the program and a budget, and the busy beaver function’s growth means no budget is generous enough to be equivalent to the real question.
• One-sided answers. Give up on always terminating, keep soundness, and you get semi-decision: a recognizer that says yes eventually when the answer is yes and runs forever otherwise. That is what a fuzzer and a symbolic executor are. Give up on completeness instead and you get the abstract interpreters (T047): always terminate, always sound, sometimes say “maybe.”
• Ranking functions. The practical technique behind every working termination checker: exhibit a value that strictly decreases on every iteration and is bounded below, and termination follows. Finding one is undecidable in general; finding one for a for i in 0..n loop is trivial, and most real loops are closer to the second case. Terminator and its descendants built a research programme on exactly this gap between “impossible in general” and “usually easy.”
• Change the model and nothing improves. Add randomness, add nondeterminism, add infinite parallelism, add a quantum computer: halting stays undecidable, because the diagonal argument never inspected the machinery. The one thing that does help is assuming a machine strictly more powerful than a Turing machine — an oracle — and then the same proof runs one level up and leaves that machine’s halting problem undecidable. The hierarchy is infinite and nothing at any level can see its own level. The boundary of this result is not a wall you can go around; it is the same wall at every altitude.

Read next