&gt; But if you want to prove runtime invariants, you usually want to prove with respect to concrete implementation, not to prove abstractly to standard.<p>Really?  I would think that if you&#x27;re trying to write a portable program, it would be much more useful to prove invariants based on the language specification, not a particular concrete implementation.