The usual idea is that while tests demonstrate the existence (and subsequent removal) of particular bugs only types (or proofs) show the non-existence of whole

The usual idea is that while tests demonstrate the existence (and subsequent removal) of particular bugs only types (or proofs) show the non-existence of whole classes of bugs. Such integer checks as you suggest are nothing more than a number paired with a proof that the number is less-than some bound. The properties of those proofs cannot be faked and their proper management and construction is all handled at compile time... Then erased. I challenge you to write a red-black tree with the RB invariants exposed in the types and then continue to say languages do not exist to protect you from yourself. The moment these things end up in types the language starts to pull back on you.