BROADCASTS.com

b'

Type safety is a basic property of both statically typed programming languages and type theories.\\xa0 It has traditionally (past few decades) been decomposed into type preservation and progress.\\xa0 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).\\xa0 Progress says that well-typed expressions cannot get stuck computationally: they cannot reduce to a form where the operational semantics is then undefined.\\xa0 This is how we model the idea that the type system is preventing certain kinds of failures: make those failures correspond to undefined behavior.\\xa0\\xa0