SML is a programming language wit a formal proof of semantics.

I prefer OCaml for it's good implementation - however good a proof, if the
programmer screwed up, or something simply got into way, the end product is
flawed.

Just my two cents...