it seems the biggest challenge for software developer is not the question how does the program work but why does it work.

tony hoare, who wrote compilers in the 60s wants to try to find an answer for this mysterious why: he called his project the verifying compiler. the goal is to construct an application, that "guarantees correctness of a program before running it".

A verifying compiler uses mathematical and logical reasoning to check the correctness of the programs that it compiles. The criterion of correctness is specified by types, assertions, and other redundant annotations associated with the code of the program. The compiler will work in combination with other program development and testing tools, to achieve any desired degree of confidence in the structural soundness of the system and the total correctness of its more critical components.

it is outlined as a grand challenge project and a lot of people wouldn't even talk about it seriously if it wouldn't be tony hoare who tries to set it up. already in the 70s some people started to work on such a compiler, but pretty soon the project got abandoned ...

the start for the project is set for 2004, 2005 or maybe in five years as he wrote somewhere, having in mind how long it took to convince people and particularly funding agencies that the genome project is of any importance. and also similar to the genome project he wants to achieve the scientific goal in 15 years.

an older paper on the topic from hoare: towards the verifying compiler