Nicolas Tabareau: Democratizing Proof Assistants

Kourou, French Guiana, June 4, 1996. European rocket Ariane 5 ignites on the launch pad for its maiden flight. 36 seconds later, the behemoth veers off its trajectory, prompting the system to trigger self-destruction. Several hundred millions of dollars go up in smoke. The culprit? A tiny computer bug that had gone completely unnoticed. “By proving software correctness, our tool is meant to prevent such accident, ” says Inria researcher Nicolas Tabareau. Based upon Type Theory and constantly improved by Inria over three decades, Coq is hailed as one of the most advanced general-purpose proof assistant worldwide. It was bestowed the Software System Award by the Association for Computing Machinery (ACM) in 2013.

A Compiler Already Available

One of the ultimate goals of this long-haul effort is to transfer the technology to the industry. As a matter of fact, a formally verified compiler for the C language is already available. Initiated by Xavier Leroy, programmed and proven in Coq, CompCert comes with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. “However, we still have to secure acceptance for the tool, Tabareau remarks. A major aircraft manufacturer has been mulling over the possibility of adopting it for a while. But first, they want to iron out the worries they have regarding this machine-checked proof, for the compiler doesn't go through the traditional testing phases. ”
As for Coq itself, although it has shown its efficiency to prove correctness of important pieces of software, it remains a rather academic tool. Its democratization suffers from a major drawback: the mismatch between equality in mathematics and in Type Theory. “In Type Theory, we consider that two terms are equal when they are syntactically the same, whereas in mathematics, we are more interested in semantic equality, in other words: the mathematical object that lies behind the syntax. ” And that has far-reaching implications. “In Type Theory, if two functions compute the same thing but are programmed differently, they can not be proven to be equal. This limitation hinders interoperability when, for instance, someone wants to import somebody else's work into his own. ”

Fascinating Connection

Against this backdrop, a recent discovery is bound to be a game-changer. Mathematician Vladimir Voevosdky has proposed an extension of Type Theory with homotopical concepts. “For the first time, it allows to get the right notion of equality in theorem provers. ”  Over the period of 2015-2019, Tabareau has been granted €1,5M by the European Research Council to explore how proof assistants could leverage this “fascinating connection ” between Homotopy Theory and Type Theory.
“Voevodsky's contribution exhibits in a sole axiom what equality must verify in order to become of semantic nature. Everybody agrees this so-called univalence axiom enables to recover everything that is needed, in particular extensional equality of functions I just mentioned. So one of our project's challenges is to replace the axiom by a computational content. Indeed one doesn't want to certify proofs with axioms but within the theory. ”

A New Research Team

Tabareau's ERC junior grant will enable him to conduct further research, in collaboration with Matthieu Sozeau,

An Inria researcher who is very instrumental in developing Coq today. The topic has prompted a keen interest throughout our community worldwide, so we will be given a lot of help, including from Thierry Coquand, Coq's first developer.

This work will span over five years and hopefully result in Coq's 9.0 version. “Being easier to use, we hope the tool will permeate the industry and gain traction among engineers at R&D level. We also wish Coq and formal verification could be taught in engineering schools, so that it would become a specialty in its own right. We'll have reached our goal the day the first COQ-LITERATE PROOF ENGINEER WANTED job offer will be published.”