Nouvelle équipe de recherche dirigée par Nicolas Tabareau à Nantes, Gallinette participe au développement de Coq. Créé il y a 25 ans par Inria, cet assistant de preuve est devenu un outil de premier plan dans son domaine. Il permet de prouver des théorèmes en mathématiques mais aussi la correction des programmes informatiques. Les scientifiques ambitionnent de répandre son usage dans l’industrie, en particulier pour la certification des logiciels critiques.

Pour se prémunir contre les bugs dans leurs logiciels, les industriels recourent massivement aux batteries de tests. Ces tests représentent souvent plus de la moitié du coût de développement. Mais il existe une alternative : prouver la correction du programme à l’aide d’un assistant de preuve. C’est tout l’objet de Coq, un des fleurons du patrimoine technologique d’Inria.

“Cet outil est basé sur l’isomorphisme de Curry-Howard, explique Nicolas Tabareau. Il s’agit d’une découverte assez fondamentale des années 1970. Elle a établi un parallèle entre les programmes et les preuves. Du coup, on s’est rendu compte qu’on pouvait définir des systèmes dans lesquels écrire un programme revenait au même que d’écrire une preuve pour une formule qui correspond à la spécification du programme. En exploitant cela à fond, on a pu concevoir un logiciel où, quand l’utilisateur est en train de programmer, il est aussi en train de prouver la spécification du programme.”

Lauréat ERC

En 2015, le scientifique a obtenu une bourse du Conseil Européen de la Recherche (ERC) afin d’étudier comment une autre découverte, la théorie homotopique des types proposée par le mathématicien russe Vladimir Voevodsky, pourrait améliorer ces assistants de preuve. “Nous commençons à avoir des résultats concrets. À la fin de l’année, nous publierons une nouvelle version de Coq. Elle comportera une modification profonde du noyau liée directement aux travaux théoriques menés dans le cadre de l’ERC. Elle aura un impact immédiat car elle va permettre de beaucoup simplifier l’utilisation. Désormais, il y a des choses que l’ordinateur est capable de comprendre comme étant vraies alors qu’auparavant il fallait les indiquer explicitement avec des preuves parallèles et des choses venant polluer le programme ou la preuve que l’on était en train de réaliser. Maintenant, l’ordinateur peut les déterminer lui-même. Du coup, cela devient transparent pour l’utilisateur.”

Dans le sillage de ces travaux, Nicolas Tabareau prend également la direction d’une nouvelle équipe-projet nommée Gallinette (1). “Notre objectif global est de démocratiser les assistants de preuve et de conforter la position de Coq sur la scène internationale.”  L’enjeu en toile de fond : convaincre l’industrie d’adopter l’outil. “Coq peut permettre aux constructeurs de prouver les systèmes critiques, par exemple les logiciels déployés dans les cockpits d’avion. Sur un pilote automatique, nous savons prouver que la commande envoyée au système est bien celle attendue par rapport aux informations fournies en entrée par les capteurs. Coq pourrait aussi servir à vérifier le bon fonctionnement des usines automatisées. Il serait intéressant de prouver que dans le cas où de petits dysfonctionnements apparaissent, les bonnes décisions sont prises pour éviter d’aller vers le pire, maintenir la cohérence de la chaîne de production et peut-être ainsi éviter sa mise à l’arrêt. Les interruptions représentent parfois un coût très élevé.”

Deep Spec

Pour l’instant, cependant, l’industrie hésite à franchir le pas. Cela dit, “depuis cinq ans, c’est dans les universités américaines que l’usage de Coq a explosé. Or, aux Etats-Unis, la frontière entre recherche et industrie est plus poreuse. Du coup, par le biais de ces universités, le logiciel commence à se diffuser dans certaines entreprises. L’un des projets les plus conséquents s’appelle Deep Spec (Spécifications Profondes). Il vise à certifier toute la chaîne de compilation qui va du langage haut niveau utilisé par le programmeur jusqu’au langage machine et même au hardware qui exécute ce langage machine.”

De leur côté, les scientifiques nantais vont aussi s’atteler à prouver Coq… par lui-même. “Si un logiciel est certifié par un ordinateur, il faut avoir confiance dans l’algorithme primitif de validation qui va dire si oui ou non une preuve est correcte. C’est cet algorithme de typage que nous souhaiterions prouver en Coq.”  L’intérêt ? “Répondre à certaines réticences des industriels qui disent : vous ne faites pas confiance à mon logiciel, alors pourquoi devrais-je faire confiance au vôtre qui est censé prouver le mien ? Nous voulons donc pouvoir proposer un programme de certification absolue. Certes, il ne sera peut-être pas très rapide mais pour les phases très critiques, il va produire le certificat ultime : celui fourni par un prouveur ayant lui-même été prouvé.”

La preuve à parité avec le test

Toujours au chapitre de l’acceptation sociale, “les industriels font d’avantage confiance au test qu’à la preuve. Nous leur avançons l’argument que ce n’est plus la peine de tester si l’on a conçu le logiciel en le prouvant. Mais ils restent frileux. Sur CompCert, le compilateur C prouvé en Coq, le chercheur Xavier Leroy s’est battu pour que ce logiciel ne soit pas contraint de passer les tests auxquels une entreprise soumettait habituellement ses programmes. Il considérait que le compilateur étant prouvé, ces tests n’avaient plus lieu d’être. L’enjeu consistait à faire accepter par l’industriel non pas tant le programme lui-même, mais plutôt le fait que la preuve était aussi légitime que le test. Nous aimerions que l’un et l’autre soit reconnus a minima comme d’égale valeur, y compris dans les normes de certification.”