I have a simple question. Can we prove that a compiler is correct? I
mean we are given a language with it's syntax and semantics and a
compiler whose correctness needs to be proved. Is this theoretically
possible?
[I think it's been done on some toy compilers, but realistic compilers
are so large that the proof would be too long to be credible. -John]
Xavier Leroy: "Formal certification of a compiler back-end, or:
programming a compiler with a proof assistant." Proceedings of POPL
2006.
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)
