Proving type safety; upcoming metatheoretic properties

Published: March 4, 2020, 9 p.m.

b'

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

'