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.)

----
Related:
* TestDrivenDevelopment
* ContinuousIntegration
* SoftwareDesignForTesting
* VerifyOutputWithGrammar
* BuildVerification
* TestAutomation
* WhiteBoxTesting
* TacticLanguage
* LanguageDescriptionsToolsApplications

----
CategoryTesting CategoryProject