From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Subject: Re: More reliable compilers (of some programming langauges) than GNAT
Date: Thu, 23 Nov 2017 09:27:08 +0100
Date: 2017-11-23T09:27:08+01:00 [thread overview]
Message-ID: <ov60os$naq$1@gioia.aioe.org> (raw)
In-Reply-To: 8760a1ek7f.fsf@nightsong.com
On 23/11/2017 04:40, Paul Rubin wrote:
> 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.
Furthermore proof of compiler correctness has nothing to do with
deciding which function is being computed. It is like deciding which
source language it was from the machine code.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
next prev parent reply other threads:[~2017-11-23 8:27 UTC|newest]
Thread overview: 24+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-11-21 15:07 More reliable compilers (of some programming langauges) than GNAT Victor Porton
2017-11-21 15:27 ` AdaMagica
2017-11-21 15:40 ` Victor Porton
2017-11-21 16:07 ` AdaMagica
2017-11-22 1:25 ` Randy Brukardt
2017-11-22 1:40 ` Randy Brukardt
2017-11-22 13:12 ` Victor Porton
2017-11-22 14:15 ` Simon Wright
2017-11-23 0:35 ` Randy Brukardt
2017-11-23 8:22 ` Dmitry A. Kazakov
2017-11-23 16:14 ` Pascal Obry
2017-11-23 17:00 ` Dmitry A. Kazakov
2017-11-28 1:09 ` Randy Brukardt
2017-11-28 9:24 ` Dmitry A. Kazakov
2017-11-22 1:19 ` Randy Brukardt
2017-11-22 2:23 ` Paul Rubin
2017-11-22 18:29 ` J-P. Rosen
2017-11-23 2:15 ` Robert Eachus
2017-11-23 3:40 ` Paul Rubin
2017-11-23 8:27 ` Dmitry A. Kazakov [this message]
2017-11-21 16:13 ` AdaMagica
2017-11-21 16:17 ` Victor Porton
2017-11-21 17:26 ` Dmitry A. Kazakov
2017-11-23 15:14 ` Robin
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox