Sure, I totally agree that there are many other invariants that you might like to prove. Many of them require full-on dependent typing—not going there for now is a choice we made to make the language approachable. (See your sibling comment for how difficult it is just to get memory safety!) But I completely agree with you that there is more to be done.