Regarding the Standard ML compiler, my question is,even though ML itself is formally defined making it possible to prove deterministic evaluations of programs, isnt the compiler itself written in C, which is not formally defined, at least not all of it? I guess my question is say we write a program in Standard ML and can prove its correctness, how do we know the C written compiler is not performing in a way that could possibly alter the results?
Thanks