Coq wins the Open Science Award for Open Source Research Software
On 5 February 2022, the French Ministry for Higher Education, Research and Innovation presented the winners of the Open Science Awards for Open Source Research Software. Developed with the involvement of teams from Université Paris-Saclay, the proof assistant Coq (http://coq.inria.fr) was awarded the prize for scientific and technical quality. As highlighted by the Ministry, “the aim of these awards is to showcase projects and research teams working to develop and share open source software and which contribute to the crucial development of the common good.”
Coq: an assistant for writing rigorous mathematical proofs
Coq is a computer language for writing mathematical definitions that can also describe data structures and algorithms. It provides an environment for the development of theorem proofs, such as the correctness of algorithms, which are fully machine-checked. Formalisations are based on libraries, meaning that a wide range of fields in mathematics and computing can be explored. Some of the major developments which have been made with the tool include the development of a proven C compiler, the demonstration of the four-colour theorem and the proof of the Feit-Thompson theorem on finite groups. Coq can also be used in cases where “manual” proofs do not provide enough guarantees, perhaps because they are derived from complex programs (i.e. automatic demonstration); because there are too many of them (i.e. program checking activities), or because they are highly technical (i.e. verifying the security of cryptographic protocols).
Collaborative development
Development for Coq began in 1984 and has continued to involve the participation of various teams and institutions. Several members of the Formal Methods Laboratory (LMF - UPSaclay, ENS Paris-Saclay, CNRS) have been closely connected to its development. Bruno Barras (Inria – the French National Institute for Research in Digital Science and Technology), Jean-Christophe Filliâtre (CNRS - French National Centre for Scientific Research) and Christine Paulin (UPSaclay, Orsay Faculty of Science) oversaw the development of the versions from 1995 to 2006 and were part of ensuring that the system be available for large academic and industrial communities around the world. Coq was the first French software to receive the ACM Software System Award in 2013. Guillaume Melquiond (Inria) is currently one of the eleven main developers of the Coq project.
Research continues at Université Paris-Saclay
At the Formal Methods Laboratory (LMF), the development of the Coq system continues. This work focuses mainly on the verification of numerical calculation algorithms and the formalisation of mathematical theorems, particularly in real analysis and number theory. It also involves the integration of automatic tools to make formal proofs accessible to a wider audience.
In the spirit of the Coq system, the teams at LMF are carrying out research on languages and environments to make defining the expected properties of programs easier, and guarantee these properties. The tools mean that it is possible to process source programs written in several languages, such as C, Ocaml, ADA and RUST.
Computer programs are omnipresent, and it is therefore essential that we have access to efficient methods and tools which allow for their behaviour to be checked safely and transparently.
For more information:
https://www.ouvrirlascience.fr/open-science-free-software-award-ceremony/
