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

Path	csiph.com!weretis.net!feeder6.news.weretis.net!news.misty.com!news.iecc.com!.POSTED.news.iecc.com!nerds-end
From	Martin Ward <mwardgkc@gmail.com>
Newsgroups	comp.compilers
Subject	Re: Are there different programming languages that are compiled to the same intermediate language?
Date	Tue, 31 Jan 2023 14:04:39 +0000
Organization	Compilers Central
Sender	johnl@iecc.com
Approved	comp.compilers@iecc.com
Message-ID	<23-01-092@comp.compilers> (permalink)
Reply-To	martin@gkc.org.uk
MIME-Version	1.0
Content-Type	text/plain; charset="us-ascii"
Injection-Info	gal.iecc.com; posting-host="news.iecc.com:2001:470:1f07:1126:0:676f:7373:6970"; logging-data="50034"; mail-complaints-to="abuse@iecc.com"
Keywords	translator, theory
Posted-Date	31 Jan 2023 12:58:22 EST
X-submission-address	compilers@iecc.com
X-moderator-address	compilers-request@iecc.com
X-FAQ-and-archives	http://compilers.iecc.com
Xref	csiph.com comp.compilers:3354

Show key headers only | View raw

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). For example:

"Provably Correct Derivation of Algorithms Using FermaT"
Martin Ward and Hussein Zedan
Formal Aspects of Computing, September 2014.
Volume 26, Issue 5, Pages 993--1031, 2014-09-01, ISSN: 0934-5043
doi:dx.doi.org/10.1007/s00165-013-0287-2
http://www.gkc.org.uk/martin/papers/trans-prog-t.pdf

> Nevertheless, I would be quite surprised if anyone could prove a
> non-toy translator correct. -John]
According to this paper: "The state of the art [as of 2014] is
the CompCert compiler, which compiles almost all of the C language
to PowerPC, ARM and x86 assembly and has been mechanically verified
using the Coq proof assistant."

Xavier Leroy. "Formally verifying a compiler: Why? How? How far?".
CGO 2011 - 9th Annual IEEE/ACM International Symposium on Code
Generation and Optimization, Apr 2011, Chamonix, France.
⟨10.1109/CGO.2011.5764668⟩. ⟨hal-01091800⟩

https://hal.inria.fr/hal-01091800

--
Martin

Dr Martin Ward | Email: martin@gkc.org.uk | http://www.gkc.org.uk
G.K.Chesterton site: http://www.gkc.org.uk/gkc | Erdos number: 4

Back to comp.compilers | Previous | Next — Next in thread | Find similar

Thread

Re: Are there different programming languages that are compiled to the same intermediate language? Martin Ward <mwardgkc@gmail.com> - 2023-01-31 14:04 +0000
  Re: Are there different programming languages that are compiled to the same intermediate language? arnold@freefriends.org (Aharon Robbins) - 2023-02-01 08:07 +0000
    Re: Software proofs, was Are there different programming languages that are compiled to the same intermediate language? Spiros Bousbouras <spibou@gmail.com> - 2023-02-05 15:14 +0000
      Re: C arithmetic, was Software proofs, was Are there different Keith Thompson <Keith.S.Thompson+u@gmail.com> - 2023-02-05 16:14 -0800
        Re: C arithmetic, was Software proofs, was Are there different gah4 <gah4@u.washington.edu> - 2023-02-06 13:26 -0800
          Re: C arithmetic, was Software proofs, was Are there different Hans-Peter Diettrich <DrDiettrich1@netscape.net> - 2023-02-07 14:31 +0100
            Re: C arithmetic, was Software proofs, was Are there different gah4 <gah4@u.washington.edu> - 2023-02-08 01:10 -0800
              Re: C arithmetic, was Software proofs, was Are there different gah4 <gah4@u.washington.edu> - 2023-02-09 00:26 -0800
                Re: C arithmetic, was Software proofs, was Are there different gah4 <gah4@u.washington.edu> - 2023-02-11 00:01 -0800
                Re: C arithmetic, was Software proofs, was Are there different drb@ihatespam.msu.edu (Dennis Boone) - 2023-02-12 04:37 +0000
            Re: C arithmetic, was Software proofs, was Are there different anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2023-02-08 10:19 +0000
              Re: C arithmetic, was Software proofs, was Are there different Hans-Peter Diettrich <DrDiettrich1@netscape.net> - 2023-02-10 19:11 +0100
                Re: C arithmetic, was Software proofs, was Are there different gah4 <gah4@u.washington.edu> - 2023-02-10 23:47 -0800
                Re: C arithmetic, was Software proofs, was Are there different anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2023-02-11 22:34 +0000
                Re: old floating point, C arithmetic, was Software proofs, was Are there different gah4 <gah4@u.washington.edu> - 2023-02-11 22:48 -0800
            Re: C arithmetic, was Software proofs, was Are there different Hans-Peter Diettrich <DrDiettrich1@netscape.net> - 2023-02-08 15:24 +0100
              Re: C arithmetic, was Software proofs, was Are there different gah4 <gah4@u.washington.edu> - 2023-02-09 00:37 -0800

csiph-web