Standard ML Proof of soundness?

Question

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

Answer 1

It is a question of responsibility. Whatever the language your SML runtime or compiler is written in (SML is a specification and an SML compiler does not have to stand on C code, it could be anything else), your responsibility is to make your SML program work according to the SML specification. If the SML compiler is buggy, that is someone else's problem.

Have you thought about the processor the compiled instructions for your SML runtime run on? Who formally proved that? And what about the electrons that move inside the processor's transistors? Who tells them to work according to the physics “laws” on which the processor's design was predicated? Who formally proved those laws?

It is not your problem.

This said, there is at the time of this writing a C compiler written essentially in Coq, CompCert. This compiler defines formal semantics for both the input language (most of C) and the target assembly languages. The input language does not have to be exactly C as long as an SML implementation is designed to work when compiled with this flavor of C. If you implemented SML in CompCert's input language, following the formal definition as closely as possible, you would have an SML interpreter with a chain of confidence that goes down nearly uninterrupted to assembly.

Answer 2

Just because you can write bad C programs doesn't mean you have to. It's perfectly possible to write a correct C program and deduce from the C language specification that the program performs correctly.