Invariants (of various kinds) are great concepts. There is a good reason you won't find these in mainstream languages though. Invariants are mind-bogglingly d

Invariants (of various kinds) are great concepts. There is a good reason you won't find these in mainstream languages though. Invariants are mind-bogglingly difficult to come up with and incrementally update. For any non-trivial code, you will be spending significantly more time thinking about invariants than implementing functionality. If you think a borrow-checker is a cognitive overhead, invariants are significantly more so. I am sure there are people who would consider than a good thing, and even argue that it results in better code in the long run. Just not enough for pushing these into mainstream languages.