Re: Verified compilers?

["Randy Brukardt" <randy@rrsoftware.com>]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1917 bytes --]

"Yannick Duch�ne (Hibou57)" <yannick_duchene@yahoo.fr> wrote in message 
news:op.v91cleyiule2fv@douda-yannick...
>Here is a quote, I'm curious to read comments about (may be from Randy ?)
>
>> According to Andrew Appel, "Part of Leroy's achievement is that he
>> makes it look like it's not so difficult after all: now that he's
>> found the right architecture for building verified compilers,
>> everyone will know how to do it."
>Quote source: http://en.wikipedia.org/wiki/Compcert
>
>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. 
The intermediate code is far simpler than Ada (or any other high-level 
language), and it is thus easy to translate correctly.

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.

In any case, no one is going to run out and totally rebuild their compiler 
because someone has found a supposedly "better" architecture for it. There 
were many such better architectures when I started out (supposely everything 
was going to be table-driven and automatically generated), and they're all 
long gone. No reason to assume that anything is different here.

                            Randy.