This blog talks about verifiable software. Here I post my thoughts on how this can be achieved, how to write a verifying compiler and what requirements must be made on the language to write code which is verifiable.
The basic requirements for a verifiable language and a verifying compiler:
– The language must allow to write highly efficient code. It should include the possibility to write functional and/or imperative code. Object orientation should be supported.
– The language must allow the software developer to express certain properties at certain points of the computation (called assertions) in order to specify what a certain part of the software has to achieve.
– The assertion language must be natural to the developer and expressive enough.
– The software developer should not be forced to supply proofs in detail, only to give proof outlines (or just to state the assertions).
– The compiler should be able to prove the asssertions of the developer or give enough information to the programmer so that he/she can fix the problem.
– Concurrency should be integral part of the language. It should be possible to statically verify liveness conditions (deadlock free, divergence free).
– The language should be scalable to allow to write very small and very large programs.
– The verifier must work in a modular way, i.e. apply only local reasoning to verify the software.
No currently available language satisfies these requirements. The closest ones are Spec# and Eiffel because they allow to express assertions. Scala is a candidate as well, because it combines functional and imperative programming very well (but it lacks assertions).
I will start with a modified version of Eiffel (so called Modern Eiffel). However the techniques shall be applicable to any other language which can be made strict enough and expressive enough.