Sites Inria

English version

Julien Thèves, Citizen Press -

Coq : la preuve par le logiciel

Récompensé par le prix SIGPLAN1 Programming Languages Software Award en janvier 2014, le logiciel Coq constitue depuis près de trente ans un support précieux pour les informaticiens qui l’utilisent comme outil d’aide à l’écriture et à la vérification de programmes. Très performant, cet assistant de preuve séduit désormais les mathématiciens.

« Coq est un outil de preuve mathématique assistée par ordinateur , expose Gérard Huet , père de ce logiciel créé au sein de l’INRIA en 1984. Au départ, il était principalement utilisé par les informaticiens pour résoudre des problèmes difficiles de correction de logiciel. Nous nous en servions également pour vérifier informatiquement des théorèmes mathématiques très simples. Mais petit à petit, avec le développement de langages informatiques de haut niveau, nous sommes arrivés à formaliser des problématiques mathématiques plus complexes.  »

Pour prouver un théorème, Coq progresse notamment en alignant des petits modules de preuve qu’il garde en mémoire, comme les briques d’un théorème plus large. Grâce à cette structure particulière, Coq a ainsi permis à Georges Gonthier de certifier en 2004 la véracité du théorème des 4 couleurs, qui affirme que toute carte dessinée sur un plan peut être coloriée avec 4 couleurs seulement. « Dans la communauté mathématique, ça a été un coup de tonnerre ! se souvient Gérard Huet. Depuis des décennies, les mathématiciens tentaient d’écrire une preuve irréfutable de ce théorème : Coq a su relever ce défi avec succès.  » Plus récemment, Georges Gonthier et son équipe ont donné une preuve, toujours grâce à Coq, du théorème de Feit et Thompson, essentiel à la théorie des groupes. Pour autant, Coq ne remplacera jamais le mathématicien. « Il ne s’agit en aucun cas d’intelligence artificielle, soutient Gérard Huet. C’est un outil qui permet la vérification formelle de théorèmes prouvés par les mathématiciens.  »

Certification de programmes informatiques

Pour autant, informaticiens et les programmeurs n’ont jamais cessé de s’y intéresser. A l’heure du tout numérique, le besoin d’applications performantes est croissant, et Coq est un outil essentiel pour garantir cette fiabilité. « L’idée, c’est d’utiliser ce logiciel pour prouver qu’un programme ne comporte aucune faute dans son exécution : en faisant cela, on certifie son exactitude, donc la rigueur de son fonctionnement, explique Yves Bertot , co-auteur avec Pierre Castéran du Coq’Art2, un livre sur l’utilisation de Coq. Quand on sait que la fusée Ariane a explosé en 1996 à cause d’une erreur de programmation, on comprend vite l’intérêt de la démarche !  »

Il y a une dizaine d’années, Coq a notamment permis à la start-up Trusted Logic , en lien avec Inria, de certifier des systèmes d’exploitation de terminaux bancaires (système Java Card). Dans le même esprit, Xavier Leroy de l’équipe Gallium a utilisé Coq pour certifier un compilateur3 C. Il travaille désormais au transfert de cet outil, dans le cadre du projet CompCert dont l’objectif est la réalisation de compilateurs certifiés. Toujours plus efficace, Coq n’a pas fini d’éclairer mathématiciens et informaticiens.

1. Special Interest Group on Programming LANguages
2. Yves Bertot, Pierre Castéran -  Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, Springer Verlag, EATCS Texts in Theoretical Computer Science, 2004, ISBN 3-540-20854-2.
3. Un compilateur est un programme informatique qui transforme un code source écrit dans un langage de programmation (ici en « C ») en langage informatique machine.

Un prix prestigieux !

A l’occasion de la conférence POPL1 qui se tiendra à San Diego (Californie) du 22 au 24 janvier 2014, le logiciel COQ va recevoir le prix SIGPLAN Programming Languages Software Award remis par l’ACM2. « Je suis très heureux de ce prix qui nous est décerné par la plus importante association professionnelle informatique, précise Gérard Huet. Coq, qui est au départ un système de preuve, reçoit un prix dans la catégorie “ langage de programmation ”. C’est comme si le langage qui sert à développer les preuves dans Coq était finalement davantage considéré aujourd’hui comme le prototype d’un langage de programmation du futur !  » Ce prix, qui récompense également un véritable travail d’équipe, tout particulièrement au sein d’Inria, sera remis aux développeurs de Coq représentés pour l'occasion par Gérard Huet , chercheur émérite et initiateur du logiciel Coq avec Thierry Coquand , ainsi qu'à Yves Bertot de l'équipe Marelle, Jean-Christophe Filliâtre , chercheur CNRS de l'équipe Toccata, et Matthieu Sozeau de l'équipe PI.R2.

1. principles of programming languages
2. Association for Computing Machinery

Mots-clés : Récompense SIGPLAN Programming Languages Software Award ACM SIGPLAN Preuve Coq

Haut de page

Suivez Inria