Im Jahr 1928 stellte David Hilbert — der einflussreichste Mathematiker seiner Generation — der Welt eine Frage: gibt es ein mechanisches Verfahren, das zu jeder mathematischen Aussage in endlicher Zeit entscheiden kann, ob sie beweisbar ist? Hilbert nannte sie das Entscheidungsproblem (englisch the decision problem) und erwartete als Antwort ein Ja. Acht Jahre später gaben ein dreiundzwanzigjähriger Doktorand in Cambridge namens Alan Turing und parallel der amerikanische Logiker Alonzo Church die Antwort: nein. Ein solches Verfahren existiert nicht. Turings Beweis verlangte zuerst, das mechanische Verfahren selbst präzise zu definieren — heute heißt es Turing-Maschine — und dann ein Problem aufzuzeigen, an dem die Maschine scheitert. Dieses Problem ist das Halteproblem.
Das Halteproblem fragt: gegeben eine Beschreibung eines Programms P und einer Eingabe I, entscheide, ob P auf I hält (terminiert) oder unendlich weiterläuft. Turings Beweis, dass kein solches Entscheidungsverfahren existiert, ist ein Diagonalargument — derselbe Mechanismus, mit dem Cantor die Überabzählbarkeit der reellen Zahlen zeigte, ein naher Verwandter der gödelschen Konstruktion. Nimm zum Widerspruch an, es gäbe ein Programm H, das (P, I) entgegennimmt und korrekt entscheidet, ob P auf I hält. Konstruiere ein neues Programm D wie folgt: D(P) ruft H(P, P) auf; sagt H „hält“, geht D in eine Endlosschleife; sagt H „hält nicht“, hält D sofort. Frage nun: was tut D, wenn es sich selbst als Eingabe bekommt? Hält D(D), so hat H(D, D) nach Konstruktion gesagt, es halte nicht — Widerspruch. Hält D(D) nicht, so hat H(D, D) gesagt, es halte — Widerspruch. Also kann H nicht existieren. Die Technik trägt weiter: der Satz von Rice (1953) zeigt, dass fast jede nichttriviale Eigenschaft des Programmverhaltens unentscheidbar ist — kein Programm kann allgemein erkennen, ob ein anderes korrekt ist, terminiert, einer Spezifikation entspricht oder fehlerfrei läuft. Die theoretische Mauer steht hart. Rekursiv aufzählbare Mengen sind solche, deren Elemente sich von einem Programm auflisten lassen; entscheidbare Mengen sind solche, bei denen auch die Nicht-Elemente auflistbar sind. Das Halteproblem ist rekursiv aufzählbar, aber nicht entscheidbar. Die Church-Turing-These besagt, dass alle vernünftigen Definitionen von „berechenbar“ zusammenfallen, was nahelegt, dass es einen einzigen kanonischen Begriff rechnerischer Mächtigkeit gibt. Die Verbindung zur gödelschen Unvollständigkeit ist exakt: beide zeigen, dass Systeme, die reich genug sind, über sich selbst zu sprechen, blinde Flecken über sich selbst enthalten, und die Beweise sind strukturell gleiche Diagonalisierungen.
Werkzeuge der statischen Analyse können im Allgemeinen nicht beweisen, dass ein Programm terminiert oder sich korrekt verhält — eine unmittelbare Folge des Halteproblems. Typsysteme in Programmiersprachen beschränken sich auf entscheidbare Fragmente des Programmverhaltens. Die formale Verifikation (Coq, Isabelle, Lean) geht am Halteproblem vorbei, indem sie dem Programmierer die Beweisarbeit abverlangt und den Beweis dann maschinell prüft — das Prüfen ist entscheidbar, das Finden nicht. Das KI-Alignment — die Frage, ob ein komplexes KI-System in allen Situationen verlässlich handelt — stößt im technischen Kern auf Unmöglichkeiten in der Form des Halteproblems. Das Halteproblem ist der Boden unter allem, was Berechnung je über sich selbst wissen kann, und es hat jeden ernsthaften Versuch, verlässliche Software zu bauen, geprägt.