[kraghen]

I have a suspicion that all non-trivial C++ programs contain undefined behaviour (e.g. not checking for or preventing overflow at every arithmetic operation involving signed integers), so trying to understand the semantics of these programs is kind of a moot point.

On the other hand, if anyone tried to formalise the semantics of C++ and prove some kind of soundness theorem they would probably find that the language definition is technically inconsistent.

Paraphrasing Feynman, if you think you understand C++ then you don't understand C++.