No I completely agree. I think it is almost a deus ex machina/wishful thinking where people wish type systems could handle invariants like this, and know at least some invariants should be easy to enforce statically, but haven't seriously considered whether all invariants generally can be feasibly statically verified at buildtime.

If they can't, then it is IMO a mistake for the language to make contracts declarative (like types), or to think of the static checks as anything more than something extra on top of what is actually a runtime check. And if they can, then why are they not just types?

Bad idea to assume "someone will write static analyzers", and use that to justify a language feature capable of expressing much more complex logic than any static analyzer would be capable of handling.