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

On 2023-01-29, Roger L Costello <costello@mitre.org> wrote:
> Hi Folks,
>
> Programming_Language_1 has a compiler which generates Intermediate_Code_1.
> Many backends are created for Intermediate_Code_1.
>
> Time passes ....
>
> Sally Smith creates Programming_Language_2. Sally wants to leverage the
> compiler work done on Programming_Language_1. She considers two approaches:
>
> 1. Create a compiler front-end for Programming_Language_2 which compiles
> instances to Intermediate_Code_1.
> 2. Create a translator which converts instances of Programming_Language_2 into
> Programming_Language_1 instances.
>
> 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?


The answer is that proving a compiler correct is the same as proving
any other software correct. What can make it it easier than some
software is that there is no real-time, nondeterministic behavior. A
compiler should produce exactly the same result every time it is
invoked with the same inputs.


Also, compilers can be written using pure functional techniques, and
this is actually "easy" to do, compared to some other kinds of
tasks. Recursion is natural for compiling because the input has a
nested, recursive structure, which the compiler follows.


Functional programs are easier to prove correct than imperative or
object-oriented programs which work by mutating the state in variables
and objects.


The compiler is expressed as a recursive function which handles all the
cases that occur (syntax shapes being translated). You can then argue
that it is correct by induction: inspect that each case is performing a
correct transformation from source language to the intermediate language
for the construct which it is handling, and that it's correctly invoking
itself recursively for the sub-expressions that the input contains.
Also included must be an argument showing that the recursion terminates.


E.g. If you know that your compiler handles, say, an if/else statement
correctly and some kind of for loop also correctly, and it's all
clean recursion, you can confidently argue that if statements nested
in loops, and vice versa, or in each other, are also handled correctly.


--
TXR Programming Language: http://nongnu.org/txr
Cygnal: Cygwin Native Application Library: http://kylheku.com/cygnal
Mastodon: @Kazinator@mstdn.ca
[I have bad news for you -- there are real compilers that produce different
results on different runs, due to things like it being loaded at different
memory addreses and hash tables of pointers end up in different orders. -John]

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