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!news.unit0.net!news.mixmin.net!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: More reliable compilers (of some programming langauges) than GNAT Date: Thu, 23 Nov 2017 09:27:08 +0100 Organization: Aioe.org NNTP Server Message-ID: References: <2fca0f38-833e-485d-9a38-febcdd507bb1@googlegroups.com> <8760a1ek7f.fsf@nightsong.com> NNTP-Posting-Host: MyFhHs417jM9AgzRpXn7yg.user.gioia.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101 Thunderbird/52.4.0 X-Notice: Filtered by postfilter v. 0.8.2 Content-Language: en-US Xref: feeder.eternal-september.org comp.lang.ada:49094 Date: 2017-11-23T09:27:08+01:00 List-Id: On 23/11/2017 04:40, Paul Rubin wrote: > Robert Eachus 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