"There are even serious discussions about whether C++ semantics can be formalized, that is, whether it is mathematically possible."

Since it is mechanisable (several compilers exist), surely it is "mathematically" possible to formalise the semantics. The question is maybe rather whether there exists a mathematically _elegant_ formalisation? Glancing at the formalisation of C in the K framework [1], I'm not sure the answer to this question is positive.

[1] https://code.google.com/p/c-semantics/

Is that "JIF" meant to be pronounced in English or French, then? ;)

"jee-f" :)

Dr. Anteater and Aunt Hillary [0] probably knew this all along.

[0]: http://themindi.blogspot.co.uk/2007/02/chapter-11-prelude-an...