Towards Engineering Proofs

A market for formal proofs is now emerging. For an example, in an ATM network, a new "ATM Transfer Capability" can be accepted as an international standard only if it comes along with some evidence that the algorithm has the intended behaviour. The ABR (Available Bit Rate) algorithm due to Christophe Rabadan was standardized because it came along with a proof, and the proof invariants are actually part of the norm. Due to the intrinsic complexity of these real-time reactive algorithms, a formal proof appears to be a must, but it currently takes several man-months to carry it out. Our objective is twofold:

- to scale up by an order of magnitude the size of the problems we can deal with;

- to downsize by an order of magnitude the time needed for a given development.

To this end, we started studying a new version of the calculus of constructions in which user-defined computations expressed by rewrite rules can be made transparent in proof terms. In addition, this new calculus will come along with an internalized notion of parameterized module, allowing the user to build, store, retrieve and instantiate parameterized proofs. Finally, we intend to develop a platform dedicated to applications in telecommunications. After recalling what theorem provers and proof checkers are, we will give a short introduction to the calculus of constructions, its current limitations, before to briefly sketch the main ideas underlying our new calculus.