From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: More reliable compilers (of some programming langauges) than GNAT
Date: Tue, 21 Nov 2017 18:23:14 -0800
Organization: A noiseless patient Spider
Message-ID: <87ine3dpbh.fsf@nightsong.com>
References: <ov1fg0$15sq$1@gioia.aioe.org>
	<2fca0f38-833e-485d-9a38-febcdd507bb1@googlegroups.com>
	<ov2jav$imm$1@franka.jacob-sparre.dk>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
Injection-Info: reader02.eternal-september.org;
 posting-host="7545848900ddf3472d52479da6781824";
	logging-data="12822"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX19dEbtCOoG2CYClmq059LGc"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux)
Cancel-Lock: sha1:0rVwz7hLpb/psIcjcs0PX0zAmCA=
	sha1:f65nlLrN8/qrUekozUQIpQP08U8=
Xref: feeder.eternal-september.org comp.lang.ada:49049
Date: 2017-11-21T18:23:14-08:00
List-Id: <comp.lang.ada>

"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.