The halting problem: why code can only be run, never read

This site will never grade your code by reading it. When you submit a solution to an exercise, the runner does not inspect your source, judge your style, or predict whether your approach is sound. It executes your code against test cases in a real runtime. The verdict comes from what happened: inputs in, outputs out, time used. That is a design decision with a theorem behind it. No program - not a compiler, analyzer, or AI - can read an arbitrary program and answer the basic question: will it ever stop? This article explains what that theorem forbids, what it leaves open, and why “run it and see” is the professional standard.

It is the second of a pair. The first, Bits have no meaning: the stored-program bargain, established the ground: in a stored-program machine, code is data, so a program can be handed to another program as input. This article follows that fact to its mathematical end.

The question no algorithm can answer

The halting problem is stated in one sentence: given a program P and an input I, decide whether P(I) ever halts. “Decide” means a single algorithm that always terminates and always answers correctly for every possible program and input. The theorem, in the standard textbook form (Sipser’s $A_{TM}$, the set of pairs $\langle M, w \rangle$ where machine $M$ accepts input $w$), says no such algorithm exists.sipser

The proof is a self-referential contradiction. Suppose a program H exists that solves the problem. Use H as a subroutine to build a program D. Given any program M, D asks H “does M halt on its own description?” It then does the opposite of what H predicts. If H says yes, D loops forever. If H says no, D halts. Run D on itself. By construction, D halts on its own description exactly when H says D does not halt on its own description. Whatever answer H gives, it is wrong. The only assumption left is H’s existence, so H cannot exist.

The proof needs one thing: the ability to feed D its own source code. That is not a trick you can perform on a machine where code and data live in separate worlds. The proof feeds a program to itself as data - meaningful only because programs have finite string encodings. The halting problem is the stored-program idea read negatively. The same maneuver that makes universal computation possible - programs as inputs to programs - makes universal analysis impossible.

The theorem’s precise shape matters. Halting is semi-decidable: positive instances are always confirmable in finite time, because you can simply run the program and wait. Negative instances are not. No finite simulation run can certify that halting will never occur, because there is no point at which “still running” becomes “never going to stop.” That asymmetry is the theorem, not a flaw in the proof. It is why the site’s runners impose a hard timeout and stop waiting: from the outside, a $2^{60}$ search and a while true loop are indistinguishable. This site’s P vs NP article makes the same point from the complexity side - you cannot tell “still working” from “never finishing,” so you bound the wait.

One piece of history needs correction because the misattribution is nearly universal. Turing’s 1936 paper - the one from the companion article - contains no halting problem.turing-1936 His machines run forever by design, printing the digits of a real number. What he proved undecidable was the circle-free problem (does the machine print infinitely many digits?) and the printing problem (does it ever print a given symbol?), the latter being computably equivalent to halting. The naming chain runs through Church (1936, where termination was built into lambda calculus as a finite reduction sequence ending in a normal form), Post (1947, who introduced the halt-by-default convention), Kleene (1952, who gave the first essentially complete statement: “there is no algorithm for deciding whether any given machine, when started from any given initial situation, eventually stops”)halting-history, Davis (1958, who coined the name “halting problem”), and Strachey (1965, the first published short self-referential proof). The drift - names stick to namers and popularizers rather than originators - matches the pattern the companion article found in the von Neumann and “Halt and Catch Fire” stories. The theorem is no less real for being mislabeled. The label just hides more history than anyone tells.

Rice’s theorem: every question about what code does

The halting problem looks like one negative result about one question. Rice’s theorem generalizes it to an entire category. Published by H. G. Rice in 1953, it states: for any non-trivial semantic property of programs - any property that depends on what a program computes, not on how its source text is written - the problem of deciding whether a given program has that property is undecidable.rice-1953 The proof is a generic reduction: from any assumed decider for the property, you build a decider for halting. The catalogue this closes off includes totality (halting on all inputs), program equivalence, emptiness of a program’s domain, and computing a fixed constant.

The engineering corollaries are direct. Working programmers meet them every day. Perfect static analysis is mathematically impossible. Analyzers must sometimes produce false positives; compilers cannot always eliminate dead code; alias analysis - whether two pointers can ever denote the same address - is undecidable even under simplifying assumptions (a result proved in 1992); antivirus software cannot catch all malware (Cohen’s 1987 theorem, with the in-the-wild consequence that containment, not detection, became the industry’s stance)cohen-1987. Even the Linux kernel’s eBPF verifier faces the documented trilemma: no verifier for a Turing-complete extension language can be simultaneously sound, complete, and decidable.

This is what the theorem says about a site like this one. The graders do not answer whether your code is correct in general, terminates on all inputs, or is equivalent to the reference solution. Those are all Rice properties, all undecidable. A grader built on them would sometimes hang and sometimes guess. Instead, the grader asks a decidable question: does this specific function produce this specific output for this specific input, in this specific runtime, within this specific time budget? The general question is impossible to answer. The specific one is execution.

What the professionals do instead

The halting problem sounds like counsel for giving up. Use it as a map. It tells you where guaranteed, general answers end and where principled alternatives begin. Verification practice uses a small set of them.

Restrict the question. Floyd-Hoare logic decomposes correctness as total correctness = partial correctness + termination. Partial correctness

• “if the program halts, the output satisfies the spec” - yields to axiomatic reasoning; termination is exactly the halting problem. So verification treats termination as a separate obligation, discharged instance by instance with human-supplied ranking arguments. This works strikingly often: Microsoft’s TERMINATOR and its successor T2 proved termination of actual Windows device drivers - real, enormous, event- driven C code - by finding the ranking functions that make their loops descend. Undecidability means no method is guaranteed. It does not mean every instance is beyond reach.

Finitize the machine. The Ethereum Virtual Machine is Turing-complete, so contract termination is undecidable in principle. The gas mechanism makes it decidable in practice by metering every execution: when gas runs out, the machine halts, turning the halting question into a bounded, checkable one. Bounded model checking does the same for hardware and software: fix a finite unwinding depth and reduce verification to SAT. Undecidability is routinely avoided by making the thing you ask about finite.

Accept a sound approximation. Abstract interpretation computes sound over-approximations of program behavior on simplified domains: no false negatives, at the price of false positives. The compiler that never eliminates quite enough dead code and the analyzer that flags things that cannot happen make the same bargain for you, invisibly.

Refuse instead of analyze. The security stack from the companion article - W^X, the NX bit, illegal-instruction traps, code signing - is the last and largest category: none of it analyzes anything. Each layer is a policy enforced by hardware that narrows what the machine will consent to run. It is an architectural admission that the general question is uncomputable, paid as a standing restriction.

The busy beaver function makes the boundary concrete. $S(n)$, the maximum number of steps a halting $n$-state Turing machine can run, is uncomputable

• it grows faster than any computable function. Yet the fifth value, $S(5) = 47{,}176{,}870$, was finally proved in 2024 by a collaboration formalizing the result in the Coq proof assistant: 27,274 lines, 638 lemmas, for a machine with five states. Five-state programs already encode open mathematical problems; the sixth value is known only to be astronomically large. The boundary is not abstract. It sits twenty-odd instructions past where human mathematics currently ends.bb5-2024

Why this site executes instead of analyzing

Every seam in this project where code is judged runs on execution, and the authoring pipeline makes the decision plain. When the exercise builder - the LLM that authors new problems - produces a solution, the platform does not trust the model’s claim that it works. The solution is executed against the problem’s test cases by the real runners, and only a solution that passes is accepted; a claim the oracle rejects is never persisted. The project’s own standing rule for the AI seams is that correctness is decided by execution, never by the LLM - exactly what the halting problem and Rice’s theorem recommend. A model can guess that code is right; only a run can establish it, and only for the cases that were run.

The learner-facing side applies the same principle. Your submission is not read and judged; it is run. The hint systems alongside the graders are LLM-driven, and they respect the same boundary: a hint can suggest, nudge, or explain - it never verdicts. The verdict comes from the run, the only thing on the decidable side of the line. This is also why the site’s lambda calculus section teaches non-termination directly. Church built termination into lambda calculus as the definition of a computation: a computation is a finite reduction sequence ending in a normal form. The canonical counterexample, $\Omega = (\lambda x.\ x\ x)(\lambda x.\ x\ x)$, reduces to itself in one step and never reaches a normal form - an infinite loop with no exit, built from nothing but the three constructs and the one rule. The introduction to lambda calculus makes the connection explicit: some computations finish, some don’t, and no algorithm can tell you in advance which is which. The site’s let-it-crash philosophy is the operational consequence: since you cannot certify that a process will not hang, isolate it. On the BEAM, an infinite loop takes down one process, and the supervisor restarts it while the node keeps running - the software equivalent of the hardware trap, applied where the math says analysis cannot reach.

LLMs and the boundary

A language model trained on programs is itself a program analyzing programs, and the theorems do not exempt it because it is large. Recent empirical work lands where the theory says it must. Benchmarked against the termination-proving competition’s suite, frontier models approach specialized symbolic analyzers at raw prediction accuracy - they are good at guessing whether a program halts - yet show a substantial gap between correct prediction and the construction of valid symbolic proofs and witnesses. That is the semi-decidability asymmetry measured on modern hardware: guessing a verdict is a heuristic task with a measurable success rate, but certifying termination is a soundness obligation that undecidability places permanently beyond guarantee. The AI-alignment literature has even begun arguing - in positions that are contested but mathematically routine - that verifying the alignment of a Turing-complete system over all inputs would require a halting oracle, by direct reduction to Rice’s theorem.

The practical moral for anyone building on LLMs is the one this site already implements: use the model for prediction, never for proof. A model can draft, suggest, explain, and guess; the run decides. When the stakes are a verdict - did the code pass, does the exercise work, is the claim true - the answer has to come from execution, because that is the only place where the answer can be checked at all.

Where to go next

• Bits have no meaning: the stored-program bargain
  • the companion article: where the code-as-data idea came from, and the second tax it levies.
• P vs NP: when a thousand cores won’t help
  • the complexity side of “you can’t tell still working from never finishing”: why timeouts, not analysis, bound the wait.
• Introducing lambda calculus - Church’s finite-reduction definition of computation, and the /lambda section’s confrontation with $\Omega$.
• Let it crash - the operational answer to states you cannot certify: isolate, restart, keep the node alive.
• Algorithms past the interview
  • what the algorithm interview is actually measuring, including the class-recognition move of “this is subset sum, so a guaranteed polynomial solution would prove P equals NP.”
• Sorting: the wall at n log n - the other member of the limits family: an information wall where this article’s is a decision wall, and neither moves for hardware.

The halting problem is often taught as a curiosity - a clever proof that some abstract machine cannot do something. Read it against the stored-program bargain. It is the price of that bargain: the same design that lets any program run on any machine also means no program can read any other and say what it will do. That is why the site runs your code instead of reading it, why the authoring pipeline executes before it accepts, and why a hint can suggest but never verdict. “Run it and see” is not surrender to the theorem. It is the theorem, understood and used.