Path: csiph.com!weretis.net!feeder6.news.weretis.net!news.misty.com!news.iecc.com!.POSTED.news.iecc.com!nerds-end From: Martin Ward 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> 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 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