2. Main applications

The previous example might suggest that Coq is mainly used to validate simple functional programs. However, this is not the case. Verification tools for dominant languages such as C, Java and Ada rely totally or more indirectly on libraries written in Coq. These tools are based on the mathematical formalization of the semantics of the programming language in question. The theorems proved once and for all in Coq guarantee either the conformity of the executable to the source, or properties such as the absence of runtime errors, the dereferencing of null pointers, or other arithmetic errors.

Without being exhaustive, we can mention a few of Coq's fields of application:

• proofs of cryptographic protocols ;

• analysis of distributed algorithms ;

• etc....