Solution (source code)

= Solution

The <halting problem> asks, given the encoding $\langle M,w\rangle$ of a <Turing machine> and an input <string>, whether that machine eventually halts on that input. Its <formal language> is
$$
\operatorname{HALT}=\{\langle M,w\rangle:M\text{ halts on }w\}.
$$
Suppose a <Turing machine> $H$ decided this <formal language>. Construct another <Turing machine> $D$ that, on an input encoding $\langle M\rangle$, runs $H$ on $\langle M,\langle M\rangle\rangle$. If $H$ answers that $M$ halts on its own encoding, $D$ enters an infinite loop. If $H$ answers that $M$ does not halt, $D$ halts. Handling malformed encodings by immediate rejection makes $D$ well-defined on arbitrary <strings>.

Now run $D$ on its own encoding. If $H$ says that $D$ halts, the construction makes $D$ loop; if $H$ says that $D$ does not halt, the construction makes $D$ halt. Either answer contradicts the assumed correctness of $H$. Therefore
$$
\boxed{\operatorname{HALT}\text{ is not a decidable language}.}
$$
The contradiction concerns a decider that must give a correct terminating answer for every encoded machine and input. Simulating $M$ does detect a halt when one occurs, but cannot in general certify that a running computation will continue forever.