Type safety

For a specified programming language and execution model, type safety commonly follows from two properties: a closed expression satisfying a typing judgment is either a value or can take an execution step, and taking a step preserves its type. Proofs proceed by structural induction on derivations, using capture-avoiding substitution for function calls. Repeated preservation keeps the remaining expression typed; the first property then rules out getting stuck at an operation outside the model's permitted cases. This argument does not imply termination or correctness of an arbitrary specification. ^[ref]