But this type theoretical definition is not really well-suited for the real world; either you have to include exceptions in the set of values, which could include even things like Segmentation Fault, making ASM well-typed, or you don't allow exceptions as values, which means that not even OCaml and Haskell are well-typed with their DivisionByZero and ArrayOutOfBounds exceptions.
Haskell (at least) is actually fine for throwing Segmentation Faults, DivisionByZero, and ArrayOutOfBounds since they can all masquerade as bottom which inhabits every type. Further, this extra inhabitant isn't (too) bad for semantics (it's "morally correct") since you cannot detect it—any attempt to examine bottom results in bottom, it's contagious.
The problem is that you sometimes can distinguish, say, a segfault from an infinite loop. Any code which does that is pretty dangerous.
That's why "pure" exceptions are considered super taboo in Haskell. If you need exception passing then you should do it in something like IO/Either/Cont to contain that effect.
It's also why the couple partial functions in Haskell are all considered warts and never for practical use:
head :: [a] -> a
tail :: [a] -> [a]
(!!) :: [a] -> Int -> a
should all be replaced by
head :: [a] -> Maybe a
tail :: [a] -> Maybe [a]
(!!) :: [a] -> Int -> Maybe a
which now uses exceptions which are marked inside the type system.
Personally, I kind of wish `(/) :: Fractional a => a -> a -> Maybe a` sometimes. It'd get confusing with IEEE floats though since that type already contains values Inf/-Inf/NaN.
To add on to tel's response, another method of supporting exceptions is to rewrite progress as "if x : t then either x |-> x', x is a value, or x is an error".
To do this, you need to define another decently large set of judgments for error propagation (such as "if x is an error and y : t then (x,y) is an error" and vice versa), but ultimately you can maintain type safety via progress and preservation while still accounting for exceptions as we know them.
On the topic of whether it would make ASM well-typed, I figure that the lack of array bounds checking would be one reason why ASM would have problems, but I haven't thought it through fully. However, I found a neat paper that tries to create a type-safe assembly language pretty similar to x86: http://www.cis.upenn.edu/~stevez/papers/MCGG99.pdf
Yes. A convenient way to do the former is to add another judgement err, so that you can prove theorems about things which go err, and know that there's nothing which isn't safe and also isn't subject to your theorems about going err. (edit: tel provides perhaps a better "irl" example)
But... that's why I added the "In the simplest case".
If you're not familiar with the "progress + preservation" definition, then it's going to be rough going understanding anything else without lots of background in logic or proof theory, especially in the case of programming languages as they relate to software engineering. As a prime example, your comment ("include exceptions in the set of values") really very often means something quite different to someone who has an intuitive grasp on the "progress + preservation" definition, and someone who does not.
See also Robert Harper's post and Michael Hicks's response on the article in question.
