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
.

Relevant Pages

  • Re: Is C99 the final C? (some suggestions)
    ... This would violate the division between preprocessor and compiler too ... much (the preprocessor would have to understand quite a lot of C semantics). ... ...This is legal C (as per the Standard), but it overflows the stack on ...
    (comp.lang.c)
  • Re: left-to-right (was In-Out Parameters for functions)
    ... >> The question is what gets lost if an evaluation order is fixed. ... What I would expect from a good compiler is factoring out the cycle ... There is no need to check program semantics very precisely. ... language may simply outlaw "pure" functions like: ...
    (comp.lang.ada)
  • Re: Glasgow haskell vs. Lispworks
    ... gotos with block structured programming and the harmfulness of goto ... How many languages even have formally-defined semantics that a compiler must ... And WRT to your dislike of Haskell: ...
    (comp.lang.functional)
  • Re: WaitForSingleObject() will not deadlock
    ... One is to hijack the semantics of volatile to disable compiler optimizations ... and otherwise let the compiler to agressive optimization. ... Agressive optimizations are the ones that work on the edge of the semantics of the ... Because the compiler can see into lock and unlock, it is able to reduce f ...
    (microsoft.public.vc.mfc)
  • Re: Glasgow haskell vs. Lispworks
    ... previous version of the compiler did" exactly as Neel did. ... You can think of "semantics" as a fancy word for the set ... If it hasn't happened with Ocaml, ...
    (comp.lang.functional)