Re: More reliable compilers (of some programming langauges) than GNAT

[Paul Rubin <no.email@nospam.invalid>]

"Randy Brukardt" <randy@rrsoftware.com> writes:
> It's possible that the application of proof tools to compilers will improve 
> their quality (especially possible in the back-ends), but there is always 
> going to be the problem of adequately expressing the correct result. 

You might like this:

    https://blog.regehr.org/archives/249

    ... I expected that we would find some flaws in CompCert’s
    formalisms. My meager experience in formal specification is that getting
    a large specification right is heroically difficult — perhaps not much
    easier than getting a complicated software system right in the first
    place. So far, however, we have found no errors in the CompCert PowerPC
    specification, their C-light specification, or in their proof
    strategy. This is pretty amazing and my opinion of the job done by the
    CompCert team is astronomically high.

It's an old article but they did in fact find some CompCert bugs back then.