Verifying Compiler

Challenge - Drawn from Computer Science:

The construction and application of a verifying compiler that guarantees correctness of a program before running it.
- http://www.verifyingcompiler.com/

Currently (2009 March) there are roughly 10 people working on VCC. It seems to be quite early stage work-in-progress, but with high probability one the most advanced projects currently trying to tackle the verifying compiler challenge

What is happening currently on this challenge?

There's much work on this topic, especially in the Coq and Agda and Maude communities. The 'Ynot' project is especially interesting for verifying programs that exhibit side-effects. Beyond that, there's also work on verification of compilers, such as Adam Chlipala's work on compiler verification (http://adam.chlipala.net/papers/ImpurePOPL10/).

It helps a lot, of course, if the language in question has a formal semantics and can effectively express the requirements to be verified. The aforementioned VCC is tackling the problem for the C language, which has many 'implementation dependent' features and unsafe, informal semantics. That makes for a difficult challenge, but likely a rewarding one due to C's popularity.

Since the halting problem is proven to be unsolvable, does that mean that the compiler will hang if it's fed source code for itself? HaHaOnlySerious. (It's a joke, but I am actually curious to know what would happen. It would be a good estimate of its power.)

CategoryTesting CategoryProject