Instead, we plan to target OCaml, a programming language whose programming model makes it relatively easier to reason about programs, while preserving the ability to produce fairly efficient code. These features of OCaml explain that it has been adopted world-wide for scientific, engineering, and financial software systems where stability, safety and correctness is of utmost importance. Examples include the Coq proof assistant, the Astrée and Frama-C static program analyzers, the CompCert optimizing C compiler, the Alt-Ergo theorem prover, financial software at Jane Street and Lexifi, or the Coccinelle semantic patch engine. The clean and simple semantics of the OCaml programming language reduces the effort involved in program verification, and this has motivated us in the recent years to focus on the development of verification tools targeting this language. These tools have now reached a degree of maturity that we believe makes them ready to tackle the challenge of developing a realistic, fully verified library of data structures and algorithms.
Although we target OCaml code, the result of our effort will not benefit only the OCaml community. Indeed, specifications and proofs of algorithms and data structures are, to a large extent, independent of the programming language. For example, a priority queue implemented in C would have essentially the same specification and invariants as its OCaml counterpart. Although in this project we plan to focus only on OCaml code, we believe that our work could be later reused, to a large extent, for developing formally verified libraries in other languages, or, even better, for developing cross-language bases of formally verified code.
Our library, which will be entirely open source, will be readily available for use by any OCaml programmer under a free software license. In particular, it will be available to implementers of safety-critical OCaml programs (e.g., Coq, Astrée, Frama-C, as well as new projects). By offering verified program components, our work will provide the essential building blocks that are needed to significantly decrease the cost of developing new formally verified programs.
To carry out our project, we gathered a team of researchers and programmers, all of whom have long experience in OCaml programming, Coq proofs, and program verification. Compared with our prior experience in program verification, we will particularly focus in this project on modularity and reusability of specifications, and on the smooth support of machine integers, which in many situations are critical for obtaining efficient code that can be realistically integrated in practical software.