Progress is what matters

It's a well-known slogan in PL theory circles that Type Soundness = Preservation + Progress. But sometimes, people just write the Preservation lemma. Sometimes they even confuse type soundness with type preservation. Richard and I were chatting today and he reminded me that the goal of a type soundness theorem is to guarantee the absence of runtime type errors. In that sense, just proving that expressions remain well-typed is skipping the punch-line. The Progress lemma tells you that, assuming you're well-typed, you'll never get stuck with a type error--that's the point!