A type system is valuable when its static judgments imply something about runtime behavior. A classic formulation of type safety proves two properties: progress and preservation.

Progress: if a closed expression $e$ is well typed, then either $e$ is already a value or it can take a computation step.

$$\vdash e:T \implies e\text{ is a value or }\exists e'.\ e\to e'.$$

This rules out well-typed programs becoming stuck on an operation with no defined behavior.

Preservation: if a well-typed expression takes a step, its type is preserved:

$$\Gamma\vdash e:T\ \land\ e\to e' \implies \Gamma\vdash e':T.$$

Together they imply that evaluation of a well-typed closed term cannot suddenly reach a stuck ill-typed state.

The proof usually follows the structure of typing and evaluation derivations. For function application, for example, progress uses the function's type to show that a value in function position must be an abstraction, while preservation uses the substitution lemma to show that replacing a typed parameter by a correctly typed argument keeps the body well typed.

“Type safe” does not mean “bug free” or “terminating.” It means the runtime behaviors excluded by the type-system theorem cannot occur in well-typed programs. The exact guarantee depends on the language's semantics and typing rules.