Good point on the Formal definition compromise.
But I think laziness-by-default has some fundamental advantages that SML pretty much loses: http://augustss.blogspot.com/2011/05/more-points-for-lazy-ev...