Re: Are there different programming languages that are compiled to the same intermediate language?

arnold@freefriends.org (Aharon Robbins)
01 Feb 2023 08:07:24 GMT

          From comp.compilers
Related articles
Re: C arithmetic, was Software proofs, was Are there different Keith.S.Thompson+u@gmail.com (Keith Thompson) (2023-02-05)
Re: C arithmetic, was Software proofs, was Are there different gah4@u.washington.edu (gah4) (2023-02-06)
Re: C arithmetic, was Software proofs, was Are there different DrDiettrich1@netscape.net (Hans-Peter Diettrich) (2023-02-07)
Re: C arithmetic, was Software proofs, was Are there different gah4@u.washington.edu (gah4) (2023-02-08)
Re: C arithmetic, was Software proofs, was Are there different anton@mips.complang.tuwien.ac.at (2023-02-08)
Re: C arithmetic, was Software proofs, was Are there different DrDiettrich1@netscape.net (Hans-Peter Diettrich) (2023-02-08)
Re: C arithmetic, was Software proofs, was Are there different gah4@u.washington.edu (gah4) (2023-02-09)
[6 later articles]
| List of all articles for this month |
From: arnold@freefriends.org (Aharon Robbins)
Newsgroups: comp.compilers
Date: 01 Feb 2023 08:07:24 GMT
Organization: non
References: 23-01-092
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
Originator: arnold@freefriends.org (Aharon Robbins)

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, 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]

Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.