> But if you want to prove runtime invariants, you usually want to prove with respect to concrete implementation, not to prove abstractly to standard. Really?

> But if you want to prove runtime invariants, you usually want to prove with respect to concrete implementation, not to prove abstractly to standard. Really? I would think that if you'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.