Towards verified extraction
Our commitment with formal verification implies a strong concern about the verification of the Coq extraction mechanism itself.
The MetaCoq project aims to do exactly that, with horizon 2022 for having a first prototype. The expected outcome is an extraction mechanism from Coq to OCaml, formally verified in Coq. This will ensure the total verification of the OCaml code obtained by our team and used in real-world applications. Our team actively supports the MetaCoq project for verification of extraction.
While this goal is not reached, we have developed a method for extracting Coq code to the OCaml in the safest way possible. The details can be found in the following article: