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

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]

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