Home Stakeholders Education Stakeholders The Coq proof assistant – formal mathematical language

The Coq proof assistant – formal mathematical language

The Coq proof assistant is a formal proof management system developed by Inria since the early 90’s.

The Coq proof assistant provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

The heart of the Coq proof assistant lies in the Curry-Howard correspondance which has put a bridge in the 50’s-60’s between proof systems and models of computations. Concretely, in the Coq proof assistant, writing the statement of a lemma is the same thing as writing the specification of a program. And more importantly, providing a proof of this lemma is the same thing as providing a program meeting the given specification.

Typical applications of the use of the Coq proof assistant include the certification of properties of programming languages (e.g., the CompCert compiler certification project, or the DeepSpec project (https://deepspec.org/) which aims at verifying full functional correctness of software and hardware), the formalisation of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching.

The Coq proof assistantCertification of properties of programming languages

Every year, software bugs cost hundreds of millions of euros to companies and administrations, as assessed by Intel Pentium division bug or Ariane 5 first flight failure. Hence, software quality is a notion that becomes more and more prevalent, going beyond the usual scope of embedded systems. In particular, the development of tools to construct softwares that respect a given specification is a major challenge of current and future researches in computer science. Interactive theorem provers based on type theory, such as Coq, equipped with an extraction mechanism that produces a certified program from a proof, are currently gaining traction towards this direction. Indeed, they have shown their efficiency to prove correctness of important pieces of software like the C compiler of the CompCert project. One main interest of using the Coq proof assistant from a computer science point of view is the ability to extract the code that has been proven directly from the proof, being able to run it as any other pieces of code. For instance, the CompCert compiler extracted from its certification is reliable and efficient, running only 15% slower than GCC 4 at optimization level 2, a level of optimization that was considered before as highly unreliable.

Formalisation of mathematics

Rubix CubeSome results in mathematics, such as the classification of finite simple groups (a.k.a. the “monster” theorem) are so technical and require such a knowledge in many areas, that you can only believe that the result is true by trusting the very mathematicians who understand the entire proof. On of the first steppingstone of the monster theorem, the Odd Order or Feith-Thomson theorem whose result can be applied to various setting such as the resolution of a Rubik’s cube, has been formalised in 2012 by Georges Gonthier’s team, after a six-year effort. It shows that it is possible to replace trust in few people by a proof certificate that can be checked by different programs, among which the Coq proof assistant, because the formal specification of the proof system is implementable. This idea of replacing proofs on paper by machine-checkable certificate has even been pushed further by Field Medalist Vladimir Voevodsky when he realised that specialists (including himself) were not able to judge whether the proof of one of his famous result was correct or not. It has lead to the univalent foundation project which aims at replacing Set Theory by Homotopy Type Theory (an extension of the theory behind the Coq proof assistant) for the foundation of mathematics.