Absolutely. Why make const char * data private in a string class otherwise? I have know it's in a valid state so I can get it to the next valid state when caller runs an operation on it.

But then a lot of proving (small p prove) an object in c++ is in a valid state amounts to hoare predicates and other spark-ada like expressions.

Certainly FP could do same and like c++ define that away when callers and callees think undefined behavior is gone?