Nicolas Tabareau : démocratiser les assistants de preuve

Kourou. 4 juin 1996. Premier vol de la fusée Ariane 5. Trente-six secondes après l'allumage, le mastodonde quitte sa trajectoire. L'autodestruction s'enclenche. Plusieurs centaines de millions de dollars partent en fumée. Le responsable ? Un petit bug informatique que nul n'avait remarqué. « En prouvant la correction des programmes, notre outil permet d'éviter ce genre d'accident », résume Nicolas Tabareau. Fondé sur la théorie des types et constamment amélioré par Inria depuis vingt-cinq ans, Coq est considéré comme l'assistant de preuve générique le plus avancé dans le monde. En 2013, il s'est vu décerner le prix du meilleur logiciel par la prestigieuse Association for Computing Machinery (ACM).

Déjà un compilateur du langage C

Un des buts ultimes de cet effort de longue haleine est d'amener l'industrie à utiliser cette technologie. De fait, un compilateur formellement vérifié du langage C est déjà disponible. Impulsé par le chercheur Xavier Leroy, développé et prouvé en Coq, CompCert apporte une preuve par l'ordinateur que le code exécutable compilé se comportera exactement comme le prévoit la sémantique du code source écrit en C. « Il nous reste toutefois à faire accepter l'outil, observe Nicolas Tabareau. Un grand constructeur aéronautique envisage de l'utiliser depuis un certain temps. Mais l'entreprise veut d'abord dissiper les inquiétudes qu'elle a vis-à-vis de la preuve certifiée par l'ordinateur, car le compilateur ne passe pas par les phases de test traditionnelles. »
En ce qui concerne Coq lui-même, bien qu'il ait démontré son efficacité à prouver la correction d'importants logiciels, il demeure plutôt un outil académique. Un inconvénient de taille contrarie sa démocratisation : la disparité entre l'égalité comme elle existe en mathématique et comme elle se définit dans la théorie des types. « En théorie des types, on considère que deux termes sont égaux s'ils correspondent syntaxiquement à la même chose, alors qu'en mathématique, on s'intéresse beaucoup plus à l'égalité sémantique. Autrement dit : l'objet mathématique qui se trouve derrière la syntaxe.  » Cette différence a de profondes implications. « En théorie des types, si deux fonctions calculent la même chose mais sont programmées différemment, alors on ne peut pas prouver qu'elles sont égales. Cette limitation constitue un frein important à l'interopérabilité, par exemple quand on veut importer les développements effectués par quelqu'un d'autre. »

Fascinante connexion

Mais une découverte récente pourrait bien changer la donne. Le mathématicien Vladimir Voevosdky a proposé une extension de la théorie des types par des concepts homotopiques. « Pour la première fois, cela permet d'avoir la vraie notion d'égalité dans les assistants de preuve. »  Sur la période 2015-2019, le Conseil Européen de la Recherche octroie une bourse de 1,5 million d'euros à Nicolas Tabareau pour explorer la façon dont les assistants de preuve pourraient s'appuyer sur cette « fascinante connexion  » entre homotopie et théorie des types.
« L'apport de Voevodsky, c'est d'avoir exhibé en un unique axiome ce que doit vérifier l'égalité pour qu'elle devienne sémantique. Tout le monde s'accorde à dire qu'avec cet axiome dit d’univalence, on récupère tout ce qu'on a envie d'avoir. En particulier l'égalité des fonctions que je mentionnais à l'instant. Un des enjeux de notre projet consiste donc à remplacer l'axiome par un contenu calculatoire dans la théorie. En effet, on ne veut pas certifier les preuves avec des axiomes mais avec ce qui est vrai dans la théorie. »
La bourse ERC starting va permettre à Nicolas Tabareau d'approfondir ses travaux en collaboration avec Matthieu Sozeau.

Un chercheur Inria très important dans le développement actuel de Coq. Le thème suscite aussi beaucoup d'intérêt de la part de notre communauté partout dans le monde. Nous recevrons donc beaucoup d'aide, y compris de Thierry Coquand, le créateur de Coq.

Ce travail s'étendra sur cinq ans et devrait donner naissance à la version 9.0 de Coq. « L'outil étant plus facile à utiliser, nous espérons qu'il se répandra dans l'industrie et chez les ingénieurs au niveau de la R&D. Nous aimerions aussi que Coq et les assistants de preuve soient enseignés dans les écoles d'ingénieurs. Il faudrait que cela devienne une spécialité à part entière. Nous aurons vraiment tout gagné le jour où l'on verra la première fois une offre d'emploi disant : RECHERCHE INGÉNIEUR PREUVE QUALIFIÉ COQ ».