L'assistant de preuves Coq est d'abord un langage informatique qui permet d'écrire des définitions et des énoncés mathématiques, de décrire des structures de données informatiques et des algorithmes. Il s’agit aussi d’un environnement pour développer des preuves de théorèmes complètement vérifiées par l'ordinateur, par exemple, la correction d'un algorithme.
Mis au point par de nombreuses équipes et institutions, Coq remporte le Prix Science ouverte du logiciel libre de la recherche 2022 dans la catégorie Science et technique. Son développement se poursuit, notamment, au sein du LMF.
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". Dix logiciels mis au point par des équipes françaises sont récompenses pour leur contribution à l'avancée de la connaissance scientifique.
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.— Le ministère de l’Enseignement supérieur, de la Recherche et de l’Innovation
Coq, une histoire de preuve formelle
Les formalisations dans Coq 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 quatre 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, initié par Gérard Huet et Thierry Coquand en 1984, s'est poursuivi avec la collaboration de nombreuses équipes et institutions : INRIA, CNRS, Université de Paris, École Polytechnique, Université Paris-Saclay, ENS Lyon, ENS Paris-Saclay.
Plusieurs membres du notre laboratoire sont étroitement liés à ce projet. Bruno Barras, Jean-Christophe Filliâtre et Christine Paulin 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 est actuellement l'un des onze membres du noyau de développeurs responsables du projet Coq.
Des recherches qui se poursuivent au LMF
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. Le LMF s'attache à proposer des méthodes et des outils performants qui permettent de contrôler leur comportement de manière sûre et transparente.