> The reality is unless you are using a formally-defined language like ML, you are relying on undefined behavior in your language. The CompCert C verified comp

> The reality is unless you are using a formally-defined language like ML, you are relying on undefined behavior in your language. The CompCert C verified compiler is a verified compiler which supports "almost all of the ISO C90 / ANSI C language" - http://compcert.inria.fr/ http://compcert.inria.fr/ . It isn't C. It is a formally-defined language that is very similar to C. It is otherwise nothing like ML.