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	William Fahle <billfahle@gmail.com>
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> (permalink)
References	<Adkz+TvWa4zLl8W9Qd6ovtClKZpZrA==> <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

Show key headers only | View raw

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]

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

Thread

csiph-web