Coq: the Program that Provides the Proof
The winner of the SIGPLAN1 Programming Languages Software Award in January 2014, the Coq program has provided invaluable support for nearly thirty years now for computer scientists who use it as an aid for writing and checking programs. This extremely efficient proof assistant has won over numerous mathematicians too.
"Coq is a computer-assisted tool providing mathematical proofs ” , in the words of Gérard Huet , the father of this program created at Inria in 1984. “Initially, it was mainly used by computer scientists to solve difficult problems encountered when correcting programs. We also used it to check by computer very simple mathematical theorems. Little by little, however, with the development of high-level computer language, we started to take on more complex mathematical problems ".
To prove a theorem, the specific approach applied by Coq is to assemble small modules of proof that it then stores in its memory as the bricks with which to construct a wider theorem. Thanks to this specific structure, Coq thus enabled Georges Gonthier to certify in 2004 the validity of the four colour theorem, which states that any map drawn on a surface can be coloured with only 4 colours. "The impact within the mathematical community was enormous!” Gérard Huet recalls. "Mathematicians had been trying to produce an irrefutable proof of this theorem for decades. Coq was successful in finding a solution ". More recently, Georges Gonthier and his team also used Coq to produce the proof for the Feit–Thompson theorem, which is essential for group theory. Nevertheless, Coq will never replace the role of the mathematician. "This has absolutely nothing to do with artificial intelligence", Gérard Huet confirms. “It is an instrument that enables the formal checking of theorems proved by mathematician ".
Certification of computer programs
Nevertheless, computer scientists and programmers have taken a constant interest in it. In an age when everything is digital, there is an increasing need for efficient applications, and Coq is an essential tool to guarantee the reliability required. "The idea is to use this program to prove that a program does not contain errors of execution. By doing so, we can certify its accuracy, and thus the reliability of its functioning”, explains Yves Bertot , the co-author with Pierre Castéran of Coq’Art2, a book about how to use Coq. “When you realise that the Ariane rocket exploded in 1996 because of a programming error, you soon understand just how useful this approach can be! "
Coq attracted a lot of attention some ten years ago now when it enabled the start-up company Trusted Logic , working in association with Inria, to certify the operating systems for bank terminals (through the Java Card system). In the same spirit, Xavier Leroy of the Gallium team used Coq to certify a3 C compiler. He is now working on the application of this tool in the context of the CompCert project, the aim of which is to produce certified compilers. With its constantly increasing efficiency, Coq is destined to continue to provide invaluable assistance to mathematicians and computer scientists alike.
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. A compiler is a computer program that converts a source code written in a programming language (in this case in "C") into a given machine computer language.
A prestigious award
During the course of the POPL1 conference to be held in San Diego, California from 22 to 24 January 2014, the Coq program will receive the SIGPLAN Programming Languages Software Award conferred by the ACM2.“I am really happy to receive such a prize from the most important professional computer association”, states Gérard Huet. “Coq, which started out as a proof assistant, will now receive an award in the 'programming language' category. It is as though the language used to develop proofs in Coq has finally come to be considered more as the prototype for the programming language of the future! " This award, which is also conferred in recognition of a fine example of teamwork, particularly inside Inria, will be presented to the inventors of Coq, represented for the ceremony by Gérard Huet , an emeritus researcher and the co-initiator of the Coq program with Thierry Coquand , and also to Yves Bertot of the Marelle team, Jean-Christophe Filliâtre , a CNRS researcher in the Toccata team, and Matthieu Sozeau from the PI.R2 team.
1. principles of programming languages
2. Association for Computing Machinery