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?

Todd Wilson

[1] Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.

[2] Daniel K. Lee , Karl Crary , Robert Harper, "Mechanizing the Metatheory of Standard ML", http://www.cs.cmu.edu/~dklee/tslf/