On me signale cet article au sujet de mon distingué collègue Byron Cook. (Byron - if you read me, don't take offense, I'm just poking fun at these articles that claim you solved the Halting Problem.)

La présentation qui est fait de ses travaux sur la preuve automatique de terminaison de programmes est assez trompeuse. L'auteur de cet article (comme d'autres journalistes avant lui) semble dire que les scientifiques, depuis Turing, pensaient le problème de l'arrêt insoluble, mais finalement se trompaient, puisque Byron est arrivé et l'a résolu.

Soupir.

Le fameux problème insoluble dont il s'agit est le problème de, étant donné un programme informatique, dire si celui-ci s'arrêtera si on l'exécute. On parle de problème de l'arrêt des machines de Turing quand on ne met pas de limitation de mémoire à la machine sur laquelle serait censée s'exécuter le programme dont on veut déterminer la terminaison.

L'impossibilité de résoudre algorithmiquement le problème de l'arrêt de Turing est une impossibilité de nature mathématique. Elle se démontre assez facilement par un petit raisonnement mathématique : on suppose que le problème de l'arrêt est résoluble, et on finit par 0=1. Autant dire que Byron n'a pas montré qu'en fait, tester l'arrêt était possible.

Ce qu'a fait Byron, c'est ce que font tous les chercheurs en analyse automatique de programmes, moi compris : devant le problème de l'arrêt de Turing et le théorème d'impossibilité (et une extension de ce théorème appelé théorème de Rice), nous contournons la difficulté. En l'espèce, ce que Byron et moi faisons, ce ne sont pas des programmes d'analyse qui peuvent répondre toujours à la question posée (termine vs ne termine pas, sort de la spécification vs reste dans la spécification...), ce qui serait impossible, mais des programmes d'analyse qui en pratique répondent dans de nombreux cas utiles.

Soupir.

Soupir.

À quand celui qui va annoncer que Church, Turing et Gödel se sont trompés quand ils disaient que l'on ne pouvait pas décider algorithmiquement si des théorèmes mathématiques sont vrais ou faux, sous prétexte qu'il y a des outils de preuve automatique ?