[AlotOfReading]

Again, you can't usefully encode "do_anything()" into a formal model. As an aside, that definition would also break the fundamental abstractions of the standard in amazingly deep ways. Regardless, my point in this particular comment thread is that eliminating undefined behavior is useful, not that I have some grudge against incompleteness.

The standards already have defined behavior that it's explicitly illegal to rely on, so I'm not sure why it's an oxymoron. Strictly conforming programs are prohibited from relying on implementation-defined behavior. You could start dealing with the issue of UB by a 3 word modification of the rules in 4-3 (N3096), though any actual attempt would have to be much more surgical to avoid undoing a decade of compiler optimizations. This isn't an easy issue and I've never pretended otherwise.

Can't say I disagree about certified compilers (though it's extremely hard to detect miscompilations via testing). Regardless, they exist and regulators/certification authorities effectively require them. Since we all have to trust the code they produce with our lives, we may as well not ignore them.