Path: csiph.com!weretis.net!feeder6.news.weretis.net!news.misty.com!news.iecc.com!.POSTED.news.iecc.com!nerds-end
From: arnold@freefriends.org (Aharon Robbins)
Newsgroups: comp.compilers
Subject: Re: Are there different programming languages that are compiled to the same intermediate language?
Date: 01 Feb 2023 08:07:24 GMT
Organization: non
Sender: johnl@iecc.com
Approved: comp.compilers@iecc.com
Message-ID: <23-02-003@comp.compilers>
References: <23-01-092@comp.compilers>
Injection-Info: gal.iecc.com; posting-host="news.iecc.com:2001:470:1f07:1126:0:676f:7373:6970"; logging-data="7064"; mail-complaints-to="abuse@iecc.com"
Keywords: translator, theory, comment
Posted-Date: 01 Feb 2023 14:38:40 EST
X-submission-address: compilers@iecc.com
X-moderator-address: compilers-request@iecc.com
X-FAQ-and-archives: http://compilers.iecc.com
Originator: arnold@freefriends.org (Aharon Robbins)
Xref: csiph.com comp.compilers:3356

I've never understood this. Isn't there a chicken and egg problem?
How do we know that the theorem prover is correct and bug free?

I ask in all seriousness.

Thanks,

Arnold

In article <23-01-092@comp.compilers>, Martin Ward  <martin@gkc.org.uk> wrote:
>On 30/01/2023 10:00, John Levine wrote:
>> [Remember that while the halting problem is insoluble in general, it's
>> often soluble in specific cases, e.g. "halt" or "foo: goto foo".
>
>More usefully, there are methods for transforming a formal
>specification into an executable implementation which
>preserve semantic equivalence, and therefore are guaranteed
>to produce a terminating program (for input states for which
>the specification is defined).    ...
[It's a perfectly reasonable question. Alan Perlis, who was my thesis
advisor, never saw any reason to believe that a thousand line proof
was any more likely to be bug-free than a thousand line program.
-John]