Proving type safety; upcoming metatheoretic properties

Type safety proofs are big confirmations requiring consideration of all your operational and typing rules.  So they rarely contain much deep insight, but are needed to confirm your language's type system is correct.  Looking ahead, this episode also talks about the different between normalization and termination when your language is nondeterministic, and the property of confluence.