Théorème impossible à prouver? Ça n’existe pas
Introduction
Vous avez forcément entendu parler le théorème des 4 couleurs qui énonce que n’importe quelle carte peut être colorée proprement avec seulement 4 couleurs. Mais est-ce que vous vous demandez aussi: est-ce vrai? N’existe-t-il vraiment aucune carte demandant nécessairement 5 couleurs ?
À vrai dire, c’est loin d’être évident. On peut essayer de le prouver soit par les calculs humains, (1936 cas différents) soit on fait l’analyse automatique par la machine. Par contre dans ce cas-là, les mathématiciens ne sont pas contents. Ils ne les avouent pas car on n’a aucun moyen de vérifier sa preuve par machine. En réalité nombreux théorèmes en maths ne semblent pas être de nature calculatoire. Donc on voudrait bien un logiciel qui peut faire la preuve lui-même et en même temps, on peut lui faire confiance.
Un outil qui va nous sauver
Alors un assistant de preuve, COQ est né pour ça. Il a été développé par une équipe française Inria, qui est décernée le prix Software System Award 2013, la plus haute distinction de l’ACM. C’est la première équipe française qui est décernée ce prix depuis 40 ans. Cet outil nous permet de prouver des théorèmes ou de les formaliser. Il nous suffit juste d’écrire un énoncé puis fournir une preuve qui sont bien sûr compréhensible par la machine, et le reste de validation sera occupé par l’ordinateur. Alors d’après Yves Bertot, directeur de recherche à Inria, l’ avancée majeure de COQ est en fait sa méthode d’éviter des erreurs de programmation qui est basée sur la logique et les mathématiques. Grâce à laquelle nous pouvons décrire ce que l’on pense de programme et des conditions attendus d’utilisation, puis on vérifie par raisonnement logique ceux qui sont vérifiés par l’ordinateur que ses conditions sont satisfaites. Mais est-ce que ça sert？
Ça sert bien sur. Premièrement on est capable de résoudre des problématiques mathématiques reconnues pour leurs difficultés, en plus on est aussi capable de faire la même chose pour les programmes. Mais vous avez peut-être une question dans votre tête, en quoi on peut garantir les vérifications des machines?
Donc ici il est inévitable de parler d’une caractéristique d’assistant de preuve: le noyau du logiciel. C’est une toute petite partie de logiciel qui joue le rôle de contrôleur de l’ensemble de l’assistant de preuve. Même s’il n’est pas capable de se certifier lui-même (théorème d’incomplétude de Godel oblige), le noyau est capable de certifier le reste de l’assistant de preuve. De plus, la taille du noyau est suffisamment petite (500 lignes environ) pour pouvoir être vérifié ensuite par un humain. Cela fait que COQ joue un rôle important dans les corrections des logiciels critiques, où produire une erreur est catastrophique. par exemple les logiciels embarqués, le secteur de robots médicaux, argent en jeu : protocoles de cartes bancaires.
Alors ,dans la future?
De nos jours on est capable de vérifier le programme et les maths, mais le COQ veut aller encore plus loin. Selon monsieur Bertot, COQ se lancera ensuite dans le domaine de recherche où il existe plus d’interactions entre les deux c’est-à-dire qu’on fait des programmes dans lesquels les mathématiques jouent un rôle important. Pour lui un domaine d’application qui fait rêver, c’est le domaine robotique.
C’est enthousiasmant de dire que tous les logiciels dans un robot sont vérifiés. N’est-ce pas?
