Part 3 · 1 chapters · ~8 min

Decidability and the Halting Problem

Decidable, semi-decidable and undecidable problems, the halting problem proved by diagonalisation, reductions between undecidable problems, Rice's theorem (every non-trivial property of program behaviour is undecidable), and what that means for linters, type checkers, static analysers and AI code review.

The proof, and what it means for tools

code

// suppose this existed and always answered correctly
declare function halts(program: string, input: string): boolean;

function trouble(p: string) {
  if (halts(p, p)) { while (true) {} }      // predicted to halt? then loop
  return;                                   // predicted to loop? then halt
}
// trouble(source of trouble): whatever halts() answers is wrong → halts() cannot exist

tool	how it copes with undecidability
type checkers (TypeScript, Rust)	sound-ish and conservative: reject some correct programs, require annotations
linters and static analysers	heuristics: report likely bugs, accept false positives and negatives
termination checkers (Coq, Lean, Agda)	accept only programs whose recursion visibly shrinks
test suites and fuzzers	check behaviour on chosen inputs; never prove absence of bugs
timeouts	give up after a budget: the practical answer to "might not halt"

Rice's theorem: any non-trivial question about what a program does (does it ever divide by zero? does it leak this secret? is it equivalent to that program?) is undecidable in general. Every analysis tool you use is an approximation by necessity, not by laziness.

WHY NO PROGRAM CAN DECIDE HALTING

proof by contradiction, in code

swipe the figure sideways, or tap expand for full screen

1/4

assume

Suppose a function halts(program, input) always returns true or false correctly.

assume a perfect deciderfor contradiction