It&#x27;s hard to retrofit this to C++.<p>This proposal has no object invariants, which are one of the most useful kinds of assertions.  Especially since you write them once for the object, and they apply to all the public function members. But then you have to clarify when control enters and leaves an object.  If you can call a public function member from another function member of the same object, you&#x27;ve re-entered the object. Does the object invariant have to be true when you do that? Spec# addressed that, but this doesn&#x27;t.<p>Function calls in assertions are a problem. You&#x27;d like to require that such functions not have side effects, so that turning off assertion checking doesn&#x27;t change program behavior.  They don&#x27;t seem to require this.<p>Trying to tighten up C++ is like trying to make a colander leakproof.  I&#x27;ve had a go at that myself.  I&#x27;ve given up and now take the position that Rust is the future.