The program that cannot be written

Could you write one program that reads any other program, plus its input, and tells you whether it will eventually stop or run forever? No. The reason fits in a few lines: hand the would-be checker a program built to do the opposite of whatever the checker predicts about it.

Why it is worth a look

The job sounds like plain engineering. Boaz Barak’s textbook, whose chapter 9 this page follows, pictures an app store that wants to reject code before it gets stuck in an infinite loop. Programmers also reason about their own loops every day. Yet the halting function (answer 1 if program M stops on input x, 0 if it runs forever) cannot be computed by any program at all. It is a limit on what programs can do, not a sign that nobody has tried hard enough.

A program that asks about itself

Two facts make the trick work. First, a program is text, so it can be fed to another program as input, including to itself. Second, one program can run any other program from its text; Barak calls this the universal machine.

Now suppose someone hands you a checker T and claims it always answers correctly. Build a new program D that does three things. It takes its own text. It asks T whether D stops. Then it does the opposite: if T says “stops”, D loops forever; if T says “runs forever”, D stops at once.

Whatever T says about D is wrong, because D was built to make it wrong. So no correct T exists. This short version appeared in print in a 1965 letter by Christopher Strachey to The Computer Journal, which Barak reprints. Strachey wrote that Turing had once told him a proof aloud, in a railway carriage in 1953, and that he had forgotten the details.

Barak also gives the longer route. List every program down the side of a table and every input across the top, and look at the diagonal: program number x run on its own text. Define a function that flips the first bit of whatever each program outputs there (treating “never stops” as 0, so the flip gives 1). No program can compute it. If one did, it would sit somewhere in the list, and on its own text it would have to output the flip of its own output. A halting checker would let you compute that function after all: ask whether program x stops on x, and if it does, run it with the universal machine and flip the bit; if it does not, answer 1. So a halting checker cannot exist either.

What it does not say

The theorem rules out one procedure that works for every program. It says nothing against deciding particular programs. A program with no loops stops, and many far subtler programs can be proved to stop or proved to loop. The claim is that no single method settles them all. Some short programs are open for a different reason: Barak points out that a few lines of Python halt exactly when Goldbach’s conjecture is false, and nobody knows whether they halt.

Why should a theorem about idealised Turing machines bind a laptop? Barak notes that programs in ordinary languages translate into Turing machines and back. That this covers every reasonable device is the Church–Turing thesis. It is a thesis, a claim about what computation is, not a theorem.

Where it came from

Turing’s 1936 paper never uses the word “halt”. His machines were meant to print the digits of a number forever. He called a machine circle-free if it keeps producing digits, and circular if it writes only finitely many. He showed that no general process can tell the two apart, by pairing a hypothetical tester with his universal machine and deriving a contradiction on the diagonal. The modern halting theorem descends from that argument.

In short

Programs are text, and a program can run another program from its text. Given any claimed halting checker, build a program that asks the checker about itself and does the opposite. The checker is wrong on that program, so no checker is right on every program. Individual programs can still be settled; a single procedure for all of them cannot exist.