The Halting Problem

Every engineer has wanted a tool that reads a program and says "this will hang". No such tool can exist. Not a slow one, not a clever one, not one from a future with faster machines. The argument fits in five sentences, goes back to Alan Turing's 1936 paper, and you can retell it at lunch.

It also sets a ceiling over every linter, type checker, antivirus scanner and static analyser you run. Each of them is wrong about some programs, by necessity rather than by bad engineering, and knowing which way each one is wrong is most of the skill in using them.

The Question

Imagine a function called halts that takes a program and an input. It returns True if the program eventually finishes on that input, and False if it runs forever. It always answers, it is always right, and it works for every program anyone could write.

This is not a timeout. A timeout can say only "not yet". The imagined function gives a perfect answer, and it may take as long as it likes to give it, provided it does finish. The claim of this topic is that no such function can be written in any language, on any machine.

The Program That Does the Opposite

Suppose halts exists. Build a second program called contrary. It takes a program as input, asks halts whether that program halts when given its own source as input, and then does the opposite. If halts says "it halts", contrary loops forever. If halts says "it runs forever", contrary returns at once.

Now give contrary its own source. If halts says contrary halts, contrary loops forever, so halts was wrong. If halts says contrary loops, contrary returns at once, so halts was wrong again. Every possible answer is wrong, so a halts that is always right cannot exist. Nothing more is needed.

def halts(program, data):
    ...                                  # imagined: always answers, always right

def contrary(program):
    if halts(program, program):         # "it halts on its own source"
        while True:                      # then loop forever
            pass
    return                               # "it runs forever": then stop at once

contrary(contrary)                       # halts cannot answer this correctly

The sketch writes the same argument as code. The first function is the imagined decider, with no body, because none can exist. The second asks the decider about its argument run on itself and does the opposite of the answer. The last line runs contrary on its own source, which is the case both branches of the figure trace to a contradiction. The code illustrates; the two paragraphs before the figure are the proof.

Why No Timeout Rescues It

A program that has run for ten seconds may finish at eleven, or at a year, or never. Waiting longer only moves the line where you give up. A timeout gives a correct answer for every program that finishes within it, and no answer at all about the rest.

The argument also does not depend on self-reference being common in real code. It is not a warning about strange programs. It shows that no single procedure is right about every program, so any real tool that answers is wrong about some of them. The self-reference is the device that finds one such program, not the place where the limit bites. Real tools are wrong about ordinary programs: loops whose exit depends on data read at run time, recursion that stops only for inputs of a certain shape, and code that waits on another process.

Rice's Theorem: It Spreads

If you could decide almost any question about what a program does, you could use that to decide halting. Take the program, arrange for it to do the thing in question only after it finishes, and ask. So none of those questions can be decided in general either. Does this function ever return None? Is this line reachable? Do these two functions compute the same thing? Does this program ever send data to that address?

Henry Rice proved it in 1953: every non-trivial property of a program's behaviour is undecidable. Questions about the text remain easy, because the limit is on behaviour. Whether a file calls eval, whether it is indented consistently and whether a name is spelled the same everywhere are all questions a tool can answer exactly, in one pass.

How Real Tools Live With It

Every analyser chooses which way to be wrong. Sound tools over-approximate: they report problems that cannot happen, like a type checker that rejects a correct program, the trade Chapter 13 described. Unsound tools under-approximate: they miss real problems, like a style linter or a signature-based antivirus. Some give up after a time or step budget and say so. Some restrict the language until the question becomes decidable, like the eBPF verifier in the previous topic.

And for one specific program, the answer can often be found. A loop that counts from 1 to 10 halts, and tools prove harder cases than that every day. The theorem forbids one method that works for all programs. It does not forbid an answer for yours. Proof assistants and termination checkers in some languages demand this: a reason, written in the code, why every loop and every recursive call gets closer to its end.

What the Ceiling Costs You

The ceiling shows up as the false positives a team learns to silence, the false negatives it ships, the "unreachable code" warning that is wrong, the antivirus that flags a new build tool and misses new malware, and the CI job with no time limit that runs for hours before the platform kills it. None of these is a bug someone will eventually fix. Each is one side of a trade that every analyser must make.

Code review, tests and timeouts exist because no tool can replace them in general. The engineering response is a bound on everything that runs and a clear picture of which side each analyser errs on, so that a sound check guards what must never slip through and a permissive one guards what only needs to be usually right.