SML is a programming language wit a formal proof of semantics. <br><br>I prefer OCaml for it&#39;s good implementation - however good a proof, if the programmer screwed up, or something simply got into way, the end product is flawed. 
<br><br>Just my two cents...<br>