Introduction to type safety

Type safety is a basic property of both statically typed programming languages and type theories.  It has traditionally (past few decades) been decomposed into type preservation and progress.  Type preservation says that if a program expression e has some type T, then running e a bit will give a result that still has type T (and type preservation would apply again to that result, to preserve the type T indefinitely along the execution of e).  Progress says that well-typed expressions cannot get stuck computationally: they cannot reduce to a form where the operational semantics is then undefined.  This is how we model the idea that the type system is preventing certain kinds of failures: make those failures correspond to undefined behavior.