Fondements théoriques

Le théorème de l'arrêt, démontré indépendamment par Alonzo Church et Alan Turing en 1936, affirme qu'aucun algorithme ne peut décider, pour tout programme M et toute entrée x, si M s'arrête. La preuve repose sur la diagonalisation, même technique que Gödel a utilisée en 1931 pour établir ses théorèmes d’incomplétude, qui avaient déjà renversé le programme de Hilbert (cohérence, complétude, décidabilité). Cette impossibilité fondamentale montre que la totalité des propriétés d’un programme ne peut jamais être connue de façon algorithmique.

H(M, x) := IF M halts on x THEN TRUE ELSE FALSE
G(y) := IF H(y, y) = FALSE THEN TRUE ELSE loop forever

En supposant l’existence de H, la construction de G conduit à une contradiction lorsqu’on exécute G(G), ce qui illustre concrètement le raisonnement de diagonalisation.

Conséquences pour la vérification logicielle

Le théorème de l'arrêt entraîne immédiatement l’indécidabilité du problème de reachability : aucun programme R ne peut, donné un autre programme M, un ensemble d’états initiaux I et une configuration cible S, déterminer si M atteindra S. Une réduction simple montre que si R existait, on résoudrait le problème de l'arrêt, ce qui est impossible.

Rice étend ce résultat à toute propriété non triviale des fonctions partielles calculées par les machines de Turing. Ainsi, il n’existe aucun algorithme capable de vérifier, par exemple, « le programme renvoie toujours le carré de son entrée ». Cette généralité implique que les outils de vérification statique ou dynamique ne peuvent garantir aucune propriété sémantique au-delà de cas très restreints.

Le théorème du Busy Beaver quantifie la difficulté : la fonction Busy Beaver, qui donne le nombre maximal d’étapes exécutées par une machine de Turing s’arrêtant, croît plus vite que toute fonction calculable. En pratique, cela signifie que même estimer la complexité temporelle maximale d’un programme est hors de portée algorithmique.

Implications pratiques et limites

Ces limites théoriques se traduisent en un coût inévitable pour la correction logicielle. Les outils de preuve formelle (Coq, Isabelle, Dafny) peuvent certifier des programmes dans des domaines restreints où les spécifications sont finies et les modèles abstraits suffisamment simples, mais ils ne peuvent pas couvrir l’ensemble du comportement d’un système général. Chaque tentative d’automatiser la vérification doit donc accepter des compromis : réduction du langage, hypothèses d’invariance, ou recours à des tests heuristiques.

En résumé, la difficulté de produire un logiciel correct ne provient pas d’un manque d’outils, mais d’une barrière mathématique inhérente à la computation. Les ingénieurs doivent combiner vérification formelle ciblée, revue de code et tests intensifs, tout en reconnaissant que la certitude absolue reste théoriquement inaccessible.