All of this just because it seemed, at some time,
a clever idea to allow the programmer to omit quantifiers?
(I know, mathematicians do this all over the place,
but it is never helpful, and especially not when teaching.)
There's your problem. Mathematicians do this specifically because it is helpful. If anything, explicit quantifiers and their interpretations are more complicated. People seem to naturally get how scoping works in mathematics until they have to figure out free and bound variables.