Path: csiph.com!weretis.net!feeder6.news.weretis.net!news.misty.com!news.iecc.com!.POSTED.news.iecc.com!nerds-end From: William Fahle Newsgroups: comp.compilers Subject: Re: Are there different programming languages that are compiled to the same intermediate language? Date: Mon, 30 Jan 2023 02:00:42 -0800 (PST) Organization: Compilers Central Sender: johnl@iecc.com Approved: comp.compilers@iecc.com Message-ID: <23-01-086@comp.compilers> References: <23-01-078@comp.compilers> MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Injection-Info: gal.iecc.com; posting-host="news.iecc.com:2001:470:1f07:1126:0:676f:7373:6970"; logging-data="52756"; mail-complaints-to="abuse@iecc.com" Keywords: translator, theory, comment Posted-Date: 30 Jan 2023 12:57:02 EST X-submission-address: compilers@iecc.com X-moderator-address: compilers-request@iecc.com X-FAQ-and-archives: http://compilers.iecc.com In-Reply-To: <23-01-078@comp.compilers> Xref: csiph.com comp.compilers:3351 On Sunday, January 29, 2023 at 10:58:58 AM UTC-6, Roger L Costello wrote: > Sally is concerned. She asks herself: > > - With either approach, how do I prove that my mapping is correct? > - For approach 1, how do I prove that the Intermediate_Code_1 that I generate > is correct for my programming language? > - For approach 2, how do I prove that the instance of Programming_Language_1 > that I generate is semantically equivalent to my Programming_Language_2 > instance?" > > What is the answer to Sally's questions? > > /Roger > [I think the answer either way is that you don't, and you try to have a test > suite that is as comprehensive as possible. -John] This is Post's Correspondence Problem, which has been proven to be equivalent to the Halting Problem, thus uncomputable. [Remember that while the halting problem is insoluble in general, it's often soluble in specific cases, e.g. "halt" or "foo: goto foo". Nevertheless, I would be quite surprised if anyone could prove a non-toy translator correct. -John]