Skip to content. | Skip to navigation

Emergences

Lettre d'information n° 37

Image emergences pour impression
Personal tools
You are here: Home 2015 Lettre d'information n° 37 Démocratiser les assistants de preuve
Document Actions

Démocratiser les assistants de preuve

Les assistants de preuve visent à prouver les théorèmes mais aussi la correction des programmes informatiques. Fruit de 25 ans de recherches par Inria, Coq est aujourd'hui l'un des logiciels en pointe dans le domaine. Toutefois, une percée en mathématique signée par Vladimir Voevosdky (médaillé Fields) pourrait ouvrir la voie à un énorme progrès de la vérification formelle. Chercheur chez Inria, Nicolas Tabareau vient de se voir octroyer une bourse du Conseil Européen de la Recherche (ERC) pour étudier comment cette découverte pourrait se concrétiser dans une version très novatrice de Coq. Comme il l'explique, ce travail devrait avoir un impact très fort et amener l'industrie à adopter cet outil de preuve.

Les assistants de preuve visent à prouver les théorèmes mais aussi la correction des programmes informatiques. Fruit de 25 ans de recherches par Inria, Coq est aujourd'hui l'un des logiciels en pointe dans le domaine. Toutefois, une percée en mathématique signée par Vladimir Voevosdky  (médaillé Fields) pourrait ouvrir la voie à un énorme progrès de la vérification formelle. Chercheur chez Inria, Nicolas Tabareau vient de se voir octroyer une bourse du Conseil Européen de la Recherche (ERC) pour étudier comment cette découverte pourrait se concrétiser dans une version très novatrice de Coq. Comme il l'explique, ce travail devrait avoir un impact très fort et amener l'industrie à adopter cet outil 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'auto-destruction 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 (1). Fondé sur la théorie des types (2) et constamment amélioré par Inria depuis 25 ans (3), 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 (4). “Pour la première fois, cela permet d'avoir la vraie notion d'égalité dans les assistants de preuve.  Sur la période 2015-2020, le Conseil Européen de la Recherche octroie une bourse de 1,5 millions 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. “Étant plus facile à utiliser, nous espérons que l'outil 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.

------
Notes :

(1) Nicolas Tabareau est membre d'Ascola, une équipe-projet conjointe d'Inria Rennes - Bretagne Atlantique et du département Informatique de l'École des Mines de Nantes. Ascola est aussi affiliée au Laboratoire Informatique de Nantes Atlantique (LINA, UMR CNRS 6241).

(2) En théorie des types, chaque terme possède un type. Les opérations sont restreintes à des termes d'un certain type.

(3) Coq bénéficie également du soutien de partenaires d'Inria: CNRS, ENS Lyon, Université Paris-Sud, École Polytechnique, Université Paris-Diderot.

(4) En topologie, deux fonctions continues d'un espace topologique à l'autre sont dites homotopiques si l'une peut se déformer de façon continue vers l'autre. Cette déformation entre deux fonctions s'appelle l'homotopie.

(5) CoqHoTT signifie: Coq Homotopy Type Theory.