Re: Verified compilers?

[Stuart <google_news@palin-26.freeserve.co.uk>]

On Tuesday, 6 March 2012 01:27:25 UTC, Randy Brukardt  wrote:
> "Yannick Duchêne (Hibou57)" <...> wrote in message 
> news:op.v91cleyiule2fv@douda-yannick
...
> >What do you think of this sentence, "now that he's found the right 
> >architecture for building verified compilers, everyone will know how to do 
> >it?"
> 
> Why would anyone want to do it? This is *not* a problem area in compilers 
> (at least in my experience). When we introduced an intermediate code to 
> separate semantics from optimization from code generation, one of the 
> unexpected benefits was that code generation bugs dropped to almost none.

I admit I have not read the report yet - so I am unaware of the scope of the 'formal verification'; and Randy's post does point out other areas where errors creep into the compilation process.  That said, there is still an issue in safety-critical applications of constructing a robust and compelling safety case, particularly covering the compilation process.  This would seem to be something that would aid in such cases.

You note 'code generation bugs dropped to almost none' - but then say:-
 
> Bugs come from incorrectly converting semantics (which could not be 
> "verified" unless a formal description of the source language exists, and 
> that has proven too hard to do for any real programming language - "a subset 
> of C" not counting as such a language!). And most of all from optimizations; 
> perhaps an optimizer could be formally verified but I suspect doing so would 
> take 3 times as much work as fixing the bugs as they're found.

The remark about optimization is interesting as [certainly up to a few years back] the number of target code generation faults seemed evenly balanced between those that were caused during optimization and those that were fixed by optimization (i.e. the fault goes away when the compiler is allowed to apply optimization strategies).

Whichever stage of the compilation process is at fault, [in my experience] there are usually a number of target code faults associated with fairly mature compilers and these cases have to be managed by the safety case and development processes.

Getting people with the experience at both the high-level source and low-level target code to review compilation issues is becoming increasingly difficult.  A technique that provides alternatives in verifying the compilation process are attractive.