Because type systems, at least in the ML tradition, reduce down to systems of logic that we already know how to prove properties about. We can prove progress an

Because type systems, at least in the ML tradition, reduce down to systems of logic that we already know how to prove properties about. We can prove progress and preservation of a type system, and we even have systems to mechanically check those proofs.