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: Wed, 22 Nov 2017 19:40:36 -0800
Organization: A noiseless patient Spider
Message-ID: <8760a1ek7f.fsf@nightsong.com>
References: <ov1fg0$15sq$1@gioia.aioe.org>
	<2fca0f38-833e-485d-9a38-febcdd507bb1@googlegroups.com>
	<ov2jav$imm$1@franka.jacob-sparre.dk>
	<dfedb193-b0bd-462d-9732-de94f0b19810@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org;
 posting-host="9a4a1f1723a50708912fa7affa5f76ea";
	logging-data="22458"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX19qg6kcQBY6kmjypFRUIktP"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux)
Cancel-Lock: sha1:gwSCyev994iYeNoHYwB3PfjQ0aE=
	sha1:h9C7Cxbp6i1pPrB8BCSdo30ae90=
Xref: feeder.eternal-september.org comp.lang.ada:49090
Date: 2017-11-22T19:40:36-08:00
List-Id: <comp.lang.ada>

Robert Eachus <rieachus@comcast.net> writes:
> The problem is that for some recursive functions, it is not possible
> to prove that the input to the compiler (in Ada) and the output (in
> machine language) compute the same function for some partially
> recursive functions.

That makes no sense at all.  It's in general not possible to prove two
arbitrary programs produce the same output.  The input and output of the
Ada compiler are not arbitrary, but in fact they are closely related, so
nothing gets in the way of such a proof.  Look at CompCert
(compcert.inria.fr) for something like that being done with a C
compiler.  It would be great to use a similar approach for Ada.