<div dir="ltr">Why doesn't Haskell (or at least "core" Haskell) have a formal definition and safety result the way Standard ML does [1], [2]? Is it just that no one has gotten around to producing them, or because there are fundamental difficulties that stand in the way of completing such a project?<div><br></div><div>Todd Wilson</div><div><br></div><div>[1] Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.</div><div>[2] Daniel K. Lee , Karl Crary , Robert Harper, "Mechanizing the Metatheory of Standard ML", <a href="http://www.cs.cmu.edu/~dklee/tslf/">http://www.cs.cmu.edu/~dklee/tslf/</a></div></div>