The halting problem is a statement about language

In 1936, Alan Turing proved that no program can decide, in general, whether other programs halt. The result is usually told as a fact about machines. The machines are nearly beside the point: the argument is about what happens when a language becomes expressive enough to describe itself.

Start with what Turing was actually asked. Hilbert's Entscheidungs problem wanted a mechanical procedure to settle any mathematical statement, and to kill the hope Turing first had to invent the mechanical procedure itself — the machine was scaffolding for a question about logic. The proof that came out fits in four sentences. Suppose a program H decides halting: given any program's text and an input, it answers correctly. Build a program D that, handed some program text p, asks H whether p halts when run on its own text — and then does the opposite. Now run D on the text of D. If it halts, H said it would not; if it runs forever, H said it would halt. H cannot exist.¹

Strip away the machinery and a shape remains, and the shape is older than computers. In 1891 @Cantor showed that no list of infinite binary sequences can contain them all: walk down the diagonal of the list, flip every bit, and the result differs from the first row in the first place, the second row in the second place, and so on down. The flipped diagonal cannot be any row. Turing's D is exactly this object — built not from a list of sequences but from a list of program descriptions.

One move, three theorems

Between Cantor and Turing sits Gödel, running the identical move inside arithmetic. By numbering formulas, @Gödel gave arithmetic the ability to talk about its own sentences, then constructed one asserting its own unprovability. Cantor diagonalized against lists of sequences, Gödel against provable sentences, Turing against computable functions. The target changes; the engine of #self-reference does not.

Look at what the engine actually requires. You need objects that can be enumerated; you need those objects to act on descriptions; and you need the system to be expressive enough to build the flipped diagonal inside itself. Turing's contribution was the third ingredient: the universal machine, which made programs into data — text that other programs can read, simulate, and contradict. The hardware is incidental. What matters is that the language of programs is rich enough to mention programs.²

This is why undecidability is not a defect any engineering can remove. Church reached the same impossibility the same year through the lambda calculus, with no tape or read-head in sight, and every formalism proposed since has inherited the theorem the moment it became expressive enough to describe its own interpreters.³ The result survives every change of machinery because it was never about machinery.

Seen this way, the halting problem is the price of expressiveness, and the price is negotiable in exactly one direction. Languages that give up power really do get decidability back: the total languages used in proof assistants reject any program they cannot see terminating, and every program they accept provably halts. The cost is that such a language cannot host its own interpreter — write one and you could diagonalize against the language from inside it. The moment #diagonalization can be phrased inside a system, the ceiling appears.

That is the theorem's real content. Full self-description and full self-prediction cannot coexist in one language; you may have either, never both. Cantor's sequences, Gödel's sentences and Turing's programs are three costumes for a single fact about description itself — and given the choice it forces, every general-purpose language humans have built has taken self-description, and paid for it with the halting problem.