Lancé il y a plus 30 ans par Inria, Coq sert à prouver la correction de programmes et de théorèmes. Il vient de franchir une étape importante avec l’ajout de nouvelles fonctionnalités améliorant sa façon d’aborder la notion d’égalité. Il devient ainsi plus facile à utiliser pour les non-spécialistes, y compris les ingénieurs dans les entreprises. Les cinq ans de travaux qui ont permis ces améliorations ont été financés par une bourse du Conseil européen de la recherche (ERC) et coordonnés par le scientifique Nicolas Tabareau. Ils arrivent dans le prolongement d’une découverte par le mathématicien et médaillé Fields Vladimir Voevodsky.
© Inria / Photo B. Fourrier
L’ordinateur prend une telle importance dans nos vies que le moindre bug peut désormais engendrer de lourdes conséquences. D’où le besoin d’outils capables de prouver que les programmes et les théorèmes sont corrects. Coq sert précisément à cela. Au niveau mondial, il est considéré comme l’un des assistants de preuve les plus aboutis. L’environnement comporte de plus un compilateur formellement vérifié du langage C. Celui-ci 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.
Pour l’instant dans Coq, quand deux fonctions calculent la même chose mais sont programmées différemment, on ne peut pas prouver qu’elles sont égales. Même si la sémantique s’avère la même, la syntaxe est différente. Il s’agit d’un problème bien identifié et hérité de la théorie des types de Martin-Löf, l’approche mathématique sur laquelle Coq se fonde.
Le mathématicien Vladimir Voevosdky y a trouvé une solution en proposant une extension de cette théorie des types à l’aide de concepts homotopiques. Sa vision expose en un unique axiome ce que doit vérifier l’égalité pour qu’elle devienne sémantique. Cette découverte théorique laisse entrevoir des répercussions concrètes. Chercheur à Inria, Nicolas Tabareau a reçu une bourse de 1,5 M€ du Conseil européen de la recherche (ERC) en 2015 pour étudier comment ce pont entre homotopie et théorie des types pourrait s’implémenter dans un assistant de preuve.
Grand bond en avant
Grâce à ces recherches, il existe maintenant des cas de raisonnement automatique (sur l’égalité ou sur la notion de non significativité de la preuve) pour lesquels le système peut désormais comprendre que certaines preuves n’ont pas d’importance en soit.
C’est le fait que la propriété est vraie qui importe, mais pas le contenu de cette preuve.
“Prenons un exemple, suggère Nicolas Tabareau. Quand on utilise des entiers machine dans une preuve, ces entiers viennent avec une preuve qu’ils sont bornés par une certaine valeur. Disons 42. On ne veut pas que sur l’outil un témoin commence à clignoter parce que, quelque part, ce même entier vient avec une autre preuve qu’il est borné par 42, et donc le système refuse de percevoir ces entiers machine comme identiques alors que manifestement ils le sont.”
Jusqu’à présent, pour surpasser ce problème de conversion dans Coq, il fallait développer un raisonnement explicite pour que l’outil accepte les deux valeurs comme étant égales. Il n’existait pas d’automatisme pour gérer simplement ce problème de conversion. “Nous avons ajouté une couche logique grâce à laquelle on peut décréter que pour certaines choses, on veut être beaucoup plus libéral sur la notion d’égalité. Deux entiers machine bornés par 42 avec des preuves différentes seront considérées comme égaux sans que l’utilisateur ait quoi que ce soit à faire.”
Dans la pratique, c’est un énorme progrès. “Le fait de prouver qu’une preuve n’a pas d’importance nécessite beaucoup de connaissances sur l’outil que l’on a pas forcément envie d’avoir si l’on est juste en train de faire une preuve sur son algorithme ou son compilateur. Les utilisateurs ont envie d’être libérés de ces lourdeurs qui peuvent sembler triviales et exagérément bureaucratiques.” Ce problème résolu, les utilisateurs peuvent maintenant se concentrer sur des raisonnements plus abstraits en lien avec leur travail.
Consortium Coq
Ces améliorations interviennent alors que l’industrie s’intéresse de plus en plus à Coq. “Un consortium a été créé récemment dans le cadre de la Fondation Inria. Il permet de recevoir des financements de la part des partenaires et de leur fournir du support technique. Plusieurs universités nous ont déjà rejoint, y compris par exemple Princeton, le MIT, Yale et U Penn aux États-Unis, ainsi que l’Institut Max Planck en Allemagne. Des discussions se déroulent aussi avec des entreprises qui envisagent de nous rejoindre. Grâce au consortium, nous avons pu recruter deux ingénieurs qui travaillent à plein temps pour répondre aux attentes de utilisateurs. L’un de ces ingénieurs, Maxime Dénès, est chargé de la gestion de la structure et l’interaction avec les partenaires.”
Outre une série de publications scientifiques et l’intégration effective des nouvelles fonctionnalités dans Coq, les travaux financés par l’ERC ont aussi contribué à augmenter la visibilité internationale de Galinette, une équipe de recherche* basée à Nantes. “Désormais nos collègues de l’étranger savent placer cette ville sur une carte et savent qu’il se passent des choses chez nous.”
Nouvelle bourse ERC
Fait notable, l’ERC vient de nouveau d’accorder une bourse à une chercheuse Inria travaillant sur la vérification formelle et la théorie des types. “Ma collègue Assia Mahboubi a obtenu une bourse Consolidator pour son projet FRESCO. Débuté en novembre 2021, ces travaux explorent des techniques de formalisation en algèbre calculatoire. Dans un domaine où l’ordinateur doit résoudre des équations et produire des solutions numériques pour ces équations, les algorithmes reposent sur des bornes de confiance qui, parfois, sont prises un peu trop vite pour argent comptant et s’avèrent fausses. Par conséquent, elle souhaite formaliser en Coq ces algorithmes pour obtenir des logiciels sûrs qui comportent des bornes de fiabilité garanties.”
|
