I really liked the post! You put into words something that I've been feeling for a long time, that IRs aren't sufficiently formal. However, I disagree with this statement:
Do we need a formal mathematical definition to avoid such ambiguities? I do not think so;
My personal belief is that they should be formally mathematically defined. Whenever there is ambiguity, it's a coin toss as to what people will decide the ambiguity really means. This isn't just a problem for different people; I've had cases where I started out thinking that an ambiguity resolved one way, then slowly (and imperceptibly to myself!) changed my view. As a result, early code acted in one way, while later code acted differently, and their combination was a bug.
Formally defined, unambiguous IR has a second benefit; we can define higher-level languages in terms of the IR, which means that the higher languages are formally defined for free1.
1The formal definition of free is 'a ridiculous amount of work defining the IR in a formal, unambiguous manner, followed by a ridiculous amount of work mapping the higher-level language(s) to the IR in a formal, unambiguous manner that also captures what we really want the higher language(s) to do'.