Yves Bertot is a senior researcher that the French Institute for Research in Computer Science and Automation (INRIA) in Sophia Antipolis and a leading researcher on correctness of software and the verification of mathematical proofs. Recently, his team was able to formally verify the correctness of the computation on the one millionth decimal digit of pi (which is 1, by the way), including a formally verifiable proof of the mathematics behind the formula and the correctness of the implementation of arithmetic operations used in the computation. We use this result as an inspiration to talk about interactive theorem proving and improving software quality.

Yves’ book with Pierre Casterán about interactive theorem proving using the Coq system is “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.