Then does ML's type system detect my "+ 1" error? Or does ML not crash once memory is exhausted? Or does "crash" in your second paragraph really mean "crash due to reading an invalid memory location"? (I'm not trying to be argumentative here; I'm trying to understand. I don't understand ML well enough to answer my questions.)

I accept Milner's claim, with his definition of "go wrong". The problem then becomes that people repeat the claim, but not the definition, and so people like me hear the claim, don't know the technical definition of "go wrong", and assume that the general meaning of the words is being used.