Re: Verified compilers?

[Jacob Sparre Andersen <sparre@nbi.dk>]

Randy Brukardt wrote:

> [...]  But I don't think that it would be all that practical to verify
> an entire compiler for a real programming language.  [...]  It surely
> would be "easy" to verify the translation of our intermediate code to
> machine code [...]

This makes me think that introducing an extra layer of intermediate
language/code might make it easier to convince yourself that each
transformation from one layer to another is correct (maybe even formally
verify it).

It would of course on the other hand introduce an extra - possibly
incorrect - transformation in the compilation system.

Can we somehow estimate the likelihood of errors in the complete
compilation system (produced software), depending on the number of
transformations involved and the procedures used to assure the
correctness of each transformation?  (Well, I know the math; multiplying
the likelihoods of each transformation being correct gives you the
likelihood that all the transformations are correct.)

But how do we estimate the likelihoods of each transformation being
correct?  Can we do better than 0.999 ** Source_Line_Count?  (Using the
rule of thumb that there on average is an error for every thousand lines
of code.)

Oh.  And who verifies that the silicon is correct?

Greetings,

Jacob
-- 
"Be who you are and say what you feel, because those who mind
 don't matter and those who matter don't mind." -- Dr. Seuss