Coq, proof assistant

In view of the growing importance of – software and hardware components – in critical areas as diverse as transport, energy, healthcare, finance, etc., the need for safe components is becoming ever more pressing.

For example, the execution of a program must be error-free under the intended application conditions: absence of runtime errors or unwanted looping, compliance with a functional specification.

However, since Turing , we have known that no algorithm can automatically take a given program and render a correction diagnosis in a finite amount of time. Consequently, only part of the software certification task can be automated. For the rest, interactive tools can be used, where the often complex –– proof of correctness must be guided by the user.

Proof assistants are interactive software programs that help users to prove theorems, relieving them of tedious and error-prone tasks. In addition to assisting with the writing of proofs, these programs check that all the proofs constructed are complete and comply with all the laws of logic.

By "theorem" we mean any kind of statement concerning either the mathematical domain or the behavior of programs written in a given language. Let's take two examples, proven in Coq:

"Any planar map can be colored with up to four colors.