The difference is that type check shows a property is universally ∀ true across all of the code, while a run time test shows a property is ∃ true in this one part of the code.