Towards the verifying compiler

In 1948 Alan Turing suggested a role for assertions in checking the correctness of large programs. In 1967, Robert Floyd suggested that a verifying compiler could check the correctness of such assertions by automatic theorem proving. Ever since, these ideas have provided a properly scientific basis for research into the problems of software engineering.

Assertions are beginning to find their way into software engineering practice. They are used mainly as test oracles, to detect programming errors as close as possible to their place of occurrence, and to prevent crashes that would be much more difficult to diagnose. I will survey the uses of assertions in current Microsoft program development. I will describe the development of programmer productivity tools based on formal analysis of large bodies of source code. I will point to current research into technology that may increase the power of these tools. The verifying compiler remains as a theoretical ideal, inspiring research for the longer term. The benefits of the research are being exploited long before the ideal is reached.