Coq: Thirty Years of Teamwork
Conceived thirty years ago at Inria's Paris-Rocquencourt laboratory, the Coq Proof Assistant continues to mobilise research teams. Its continuous development is a testimony to the interest shown in it by both the scientific community and, more recently, the financial sector.
1984: Thierry Coquand , a researcher on the Formel project directed by Gérard Huet , lays the foundations in his thesis of a powerful logical structure called the "Calculus of Constructions". The team then develops a functional programming language, Caml, and on this basis starts to construct a proof development environment within the Calculus of Constructions, initially called "CoC" and later becoming known as "Coq". This is the start of a major scientific adventure, many contributions to which will be made over the years by several generations of researchers originating not only from Inria but also from a wider cross-section of the French university world.
In 1991, within the Coq team, Christine Paulin-Mohring pursues the development of the program, using as a basis a more expressive logical structure, the Calculus of Inductive Constructions, and then taking over from Gérard Huet as head of the team in 1996. "Coq has a long history behind it”, reflects Christine Paulin-Mohring. “In the 1990s, researchers such as Chet Murthy and Jean-Christophe Filliâtre greatly contributed to its construction ". Now a researcher in the Toccata team and a lecturer at Paris Sud University, Christine Paulin-Mohring continues to use Coq regularly. "Coq is both a programming language and a mathematical proof assistant. This is its great strength”, she considers. “As a computer scientist and a mathematician, Coq offers me the best of both worlds. It is a tool that can be used to really get to the bottom of things. In particular, it allows our computers to work better and with better-constructed program ".
In the early 2000s, Bruno Barras and Hugo Herbelin take over responsibility for developing Coq. As an indication of the prestige the project enjoys within Inria, it is allocated a technological development action (ADT), a mechanism designed to provide support for major cross-disciplinary and collaborative projects by providing them with the relevant human and technical resources. Under the leadership of Hugo Herbelin since 2006, several Inria teams now participate in developing the program PI.R2 in Paris and Toccata in Orsay, in addition to the Marelle team directed by Yves Bertot and including researchers at the LIX laboratory in Palaiseau and at the Inria centre in Sophia Antipolis.
Apart from those involved in its development, numerous scientists use it on a daily basis within the framework of their research. This is the case for Daniel de Rauglaudre , a research engineer in the Aoste team. "I'm currently using Coq to prove the Puiseux theorem, which defines the solutions for certain types of polynomial equations. I'm progressing step by step, since Coq requires an extremely rigorous approach", he adds. “The program controls the mathematicians' activities and won't tolerate any type of imprecision! "
The Coq program is also used to check that programs are accurate in terms of their specifications. It is thus extremely useful for industrial operators and departments that need to certify the security of their IT systems. It has thus been used to certify the Java Card environment of electronic payment terminals using smart cards (Trusted Logic, SUN, and GEMALTO).