Mathematicians have a relatively fluid relationship with notation. Since higher math is constantly introducing new abstractions, or applying new techniques to old abstractions, new notation is introduced, or old notation reused in a slightly different way in a large percent of papers that are influential. I think mathematicians would happily admit that.

That said, it does bring me back to a math class where a professor, after realizing he needed to introduce a subscript, to a subscript, to a subscript of something that had both a subscript and superscript already, made a comment along the lines of "please excuse my poor notation."

I certainly agree with this that it is inconsistency. With a straight up notation handbook and agreed upon "language" I would have been happy to get over the hump once, maybe twice, but when I spend 15 minutes re-assuring yourself that the notation in this proof/formula/paper is just a variation of another equivalent notation, it makes me irritated and that interferes with my appreciation of the concepts being presented. Do it enough and I just throw the paper out.

There was some point in my education where I was taking three classes, each with their own definition of phi. It drove me nuts.

Coq notation, lisp-style notation, even python-style notation- anything would be better.

I remember taking three classes: informal logic (philosophy) which ended up talking about formal logic anyway, electrical engineering, and a math class. It make the logic class really easy, already knowing it from EE. They all had different notation for 'implies', 'not', 'and', 'or', etc. You could argue that the computer languages have a 4th notation, but I won't.

You're confusing pedantry with rigor. The fact that a compiler will complain at you if you misspell 'continue' but a mathematical proof will keep going just fine doesn't mean that programming is more 'rigorous' than mathematics.