Our project aims at developing the first mechanically verified library of efficient general-purpose data structures and algorithms. This may come as a surprise, but there does not currently exist any verified library of significant size in any programming language. In the recent decades, a lot of effort has been invested into the development of program verification tools for mainstream languages such as C or Java, including efforts by members of our teams. These efforts have been successful in a number of specific application domains, and they are relevant (and even necessary) for the purpose of verifying low-level code. However, the task of verifying, and even specifying, code written in such languages is often severely burdened by the intrinsic complexity of the semantics of the underlying programming model, such as the numerous possibilities for memory access patterns in the C language. This complexity probably explains in part the lack of verified libraries for such languages.
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.
