Coq, lauréat du Prix « science ouverte du logiciel libre de la recherche »
Le 5 février 2022, le ministère de l’Enseignement supérieur, de la Recherche et de l’Innovation a remis pour la première année les Prix « science ouverte du logiciel libre de la recherche ». L'assistant de preuves Coq, que des équipes de l’Université Paris-Saclay ont contribué à développer, a remporté ce Prix dans la "qualité scientifique et technique". Comme indiqué par le ministère, : "L'objectif de ces prix est de mettre en valeur les projets et les équipes de recherche qui œuvrent au développement et à la diffusion des logiciels libres et qui contribuent à la construction d’un bien commun de première importance."
Coq : un assistant pour écrire des preuves mathématiques rigoureuses
Coq est d'abord un langage informatique qui permet d'écrire des définitions et des énoncés mathématiques mais aussi de décrire des structures de données informatiques et des algorithmes. Il s’agit d’un environnement pour développer des preuves de théorèmes, comme la correction d'un algorithme, qui sont complètement vérifiées par l'ordinateur.
Les formalisations s'appuient sur des bibliothèques qui permettent d'aborder des champs variés des mathématiques et de l'informatique. Parmi les développements de grande ampleur réalisés à l'aide de cet outil, on note le développement d'un compilateur C prouvé, la démonstration du théorème des 4 couleurs ou encore la preuve du théorème de Feit-Thompson sur les groupes finis.
Coq est également utilisé dans des situations où les preuves "à la main" n'offrent pas suffisamment de garanties, par exemple parce qu'elles sont issues de programmes complexes (comme en démonstration automatique) ou parce qu'elles sont en nombre trop important (dans les activités de vérification de programmes) ou encore parce qu'elles ont un niveau important de technicité (justification de la sécurité des protocoles cryptographiques).
Un développement collaboratif
Le développement de Coq a débuté en 1984 et s'est poursuivi avec la collaboration de nombreuses équipes et institutions. Plusieurs membres du Laboratoire Méthodes Formelles (LMF-Univ Paris-Saclay, ENS Paris-Saclay, CNRS) sont étroitement liés à cette histoire.
Bruno Barras (Inria), Jean-Christophe Filliâtre (CNRS) et Christine Paulin (Univ. Paris-Saclay, Faculté des Sciences d'Orsay) ont été responsables du développement des versions de 1995 à 2006 et ont contribué à ce que ce système soit utilisable par une large communauté académique mais aussi industrielle et ceci dans un contexte international.
Le système Coq a ainsi été le premier logiciel français à recevoir l'ACM Software System Award en 2013. Guillaume Melquiond (Inria) est actuellement l'un des onze membres du noyau de développeurs responsables du projet Coq.
Des recherches qui se poursuivent à l’Université Paris-Saclay
Au LMF, les contributions au système Coq se poursuivent. Elles portent principalement sur la vérification d'algorithmes de calcul numérique et la formalisation de théorèmes mathématiques notamment en analyse réelle et en théorie des nombres. Elles concernent aussi l'intégration d'outils automatiques afin de rendre la preuve formelle accessible à un plus large public.
Dans la suite et dans l'esprit du système Coq, les équipes du LMF effectuent des recherches sur des langages et environnements pour faciliter la définition des propriétés attendues des programmes et garantir ces propriétés. Les outils permettent de traiter des programmes source écrits dans plusieurs langages comme C, Ocaml, ADA ou RUST et, pour certains d'entre eux, sont déjà utilisés dans un contexte industriel.
Les programmes informatiques sont omniprésents, il est donc essentiel de disposer de méthodes et d'outils performants qui permettent de contrôler leur comportement de manière sûre et transparente.
