Abstract
Last year, the Prove&Run team demonstrated the feasibility of full proof of a microkernel, Minix V3, of a complexity comparable to that achieved by the NICTA team on Sel4 - a hitherto unrivalled world first. We used a different approach to take into account new constraints crucial to the use and, above all, the generalization of this kind of proof in an industrial environment. The longer-term aim of Prove&Run is to demonstrate and enable the large-scale use of formal methods for the development of critical components.
Scaling up formal methods requires additional constraints to be taken into account for critical applications. For example, while it is crucial to make at least the first manned flight to Mars before imagining the first regular link between Mars and Earth, acceptable methods for the first experimental shuttle will not necessarily be acceptable for the first commercial shuttle. In the same way, we came to the conclusion that we needed to develop a new language and a new approach, based essentially on the state of the art in formal methods, on the prodigious knowledge accumulated over the last few decades in this field and more broadly in theoretical computer science. But we also concluded that certain features considered to be "must-haves" in the academic world should be dropped, as they seemed too costly at the present time in view of the specific constraints of the industrial context. For example, we decided not to use the higher order, at least initially. We have also departed from the tendency to eliminate loops in program descriptions: our function definitions are not necessarily recursive and can adopt an imperative style, while the language remains functional.
