Re: Verified compilers?

[Shark8 <onewingedshark@gmail.com>]

On Feb 21, 9:42 am, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> 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?”
>
> --
> “Syntactic sugar causes cancer of the semi-colons.” [1]
> “Structured Programming supports the law of the excluded muddle.” [1]
> [1]: Epigrams on Programming — Alan J. — P. Yale University

I think the sentence shows a bit of solipsistic thinking on the part
of the writer's view of languages; as everyone on this thread ought to
know Ada's had verified compilers since its first implementations. (I
am using 'verified' and 'certified' rather interchangeably here, if
that's not the case though I'd like to hear what exactly the
difference is.)