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

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.