Re: Compiler Correctness

Hans-Peter Diettrich a écrit :


> Otherwise a proof of the correctness of any program must take into
> account the detailed behaviour of the host machine, and then is valid
> only for that specific machine. IMO it's much simpler to write
> machine-independent compiler code, instead of proofing the behaviour of
> machine-dependent code, for every new host machine ;-)


I am not expert in proving systems, but I am unsure that writing
machine-independent code would fundamentally help for certifying a
compiler: isn't like compiling for a virtual machine ?


Personally I think that, unless you compile for Turing machines (which
is impossible in practice because of memory space limitation), I doubt
that we can provide a full proof that is 100% mathematically
guaranteed with classical proofs (as we had all learn in school): you
would always have to make a set of assumptions that makes your life
easier. The question is how much and which assumptions are you ready
to admit. As said Xavier in his reply, you have for instance to assume
that the arithmetic of the target processor behaves as expected by the
compiler or by your prover. This is an acceptable assumption because
we generally trust processor vendors (do we have the choice ?),


Each real target machine (whether it is a virtual machine or not) is a
simplification of a Turing machine. Consequently the semantics of the
arithmetic computation on any of these real machines is not the
semantics of the computation used in mathematics. You have then to
mathematically define a new semantics for arithmetic computation. Unless
you use your brain (and you get a job for eternity), it's your own
machine that will implement this semantics and use it for certifying
your compiler... This come back to trust the hardware implementations of
processor vendors. Finally, by following the famous nomenclature of
Xavier's proofs classifications, we can name it "proof by (commercial)
power" or "proof by resignation" :-)


S

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