Verifying compiler

Verifying compiler is a great challenge proposed by C. A. R. Hoare. Currently it is a challenge to make a correspondence between the theory of computing and software applications. The development of a verifying compiler is an essential tool to bring both areas together, since it would make the theoretical results achieved available to software engineers.

Great challenges

A grand challenge is a coordinated or competing effort that may lead to far-reaching scientific achievements that could not have been achieved otherwise.

• Demonstrate the last theorem of Fermat (complete)
• To reach the moon in 10 years (completed)
• Cure cancer in 10 years (fallen in the 1970s)
• Create the map of the Human Genome (completed)
• Create the map of Human Proteoma (too difficult at the moment)
• Find the Higgs Bonus (in progress)
• Find gravitational waves (in progress)
• Unify the four forces of physics (in progress)
• Hilbert's Program for the Basics of Mathematics (abandonado in the 1930s)

Great challenges in computing

• Prove that P is different from NP (open)
• The Turing test (not reached)
• The verifying compiler (abandonado in the 1970s)
• Chess Champion Program (completed in 1997)
• Program to play Go at professional level (completed in 2016)
• Automated translation between two languages (falled in the 60s, quite advanced today)

Characteristics of a great challenge

• Project for at least fifteen years
• Global participation
• Clear criteria of success or failure
• Fundamental advances in science or engineering

Required conditions

• Enough maturity in the area
• General support of the scientific community
• Sustained commitment of participants
• Awareness of the importance of funding agencies

The Verifying Compiler

• The compiler verifies the correctness of the programs regarding their specification.
• The specification is given as assertions in the program, type information, etc.
• The tools used for verification are tools for supporting mathematical and logical reasoning.

This is a challenge that was already formulated by Turing (1948), McCarthy (1962), Floyd (1967), etc.

It represents an engineering achievement of something that was once considered unachievable or impractical.

Measure of success

• Mechanical verification of a set of representative examples of mechanically verified software tools.
• Each example produced must be able to replace existing software in its routine use, so as to serve as a basis for future developments.
• A prototype checker must be available to the community.

Hoare proposes as a minimum the verification of correctness and completion of applications of at least ten thousand lines, and with a lower level of security up to the treatment of applications of at least one million lines.