> I can't rationalize how "prevents... except" isn't still just heuristics.

“Prevent something unless obviously safe” is a core pattern of rules in type systems. For example variable assignment in Java. If it’s possibly unsafe (RHS is not a subtype of LHS) then it’s prevented.

Are you saying Java and all of classic type theory is just heuristics?