I found thinking in terms of Mathematica and MatLab helped me think about math syntax as it is more complete.
You will find algorithms written in mathematics (to prove a certain fact, sometimes we exhibit a procedure that is guaranteed to accomplish it) and they are generally clear and easy to read with simple syntax, etc -- the actual mathematics is in the proof that the algorithm is correct, or always terminates.
Basically something that takes http://arxiv.org/archive/math or http://www.ncbi.nlm.nih.gov/pmc/ where the user can view and annotate the PDF format,
Where you can also click on mysterious/not-yet-grokked variable, and it'll take you to the definition of that variable or the previous entry of derivation,
Maybe also add some cool dank meme's on some science or math trivia of the back-story of the author/MC of the paper/citation.
You're definitely right that mathematics doesn't really have things like variables though. You're only allowed to define a symbol once, but then it doesn't necessarily need to have a specific value (e.g. you're allowed to define 'x' and 'y' implicitly using the equation 'x = 2yx', or less trivially 'x^2 + y^2 = 1').
The only arguably true parts are that mathematics can't be 'run' with regular programs, and most text editors can't handle it too well. This is largely because mathematics predates software.
Of course before computers even existed it was proven that any mathematical proof could be verified on a computer, and editors that could typeset mathematics predate most programming languages.
I'm sure computer assisted and computer annotated proofs will advance marvellously over the coming decades, but it seems incomprehensible to me that modern research mathematics could be done within that framework.
It would be interesting to be proved wrong, but it seems that the skills required to use the current level of proof assistants would be much like asking modern web programmers to use front panel toggle switches. Toy programs would be onerous, but possible. Anything with any real content would require specialists in the assistant language. Suddenly you're asking mathematicians to be programmers as well, albeit in a specialised language.
From what I've seen, it's still like programming in assembler. Or worse. I've seen and have had some training in proof-assistant languages, and at their current status it just seems hopeless for real work.
I look forward to seeing how it will develop over the coming decades, although I doubt I will still be a working programmer, or mathematician, by the time it becomes possible to express mathematics at the highest level in proof assistant languages.
Despite disagreeing with it, here is the text:
================================================================
Imagine if I asked you to learn a programing language and a culture of practices
where:
- All the variables were a single letter, pathologically so, and that programmers
enjoyed using foreign alphabets, glyph variation and fonts to disambiguate their
code from meaningless gibberish.
- None of the functions were documented independently, and instead the API
documentation consisted of circular references to other pieces of similar
code, often with the same names overloaded into multiple meanings, often
impossible to Google.
- None of the sample code could be run on a typical computer, in fact, most
of it was pseudo-code lacking a clear definition of input and output, or
even the environment and domain in which it is typically expected to be run.
- Expressive code in this language was impossible to write in a typical text
editor or word processor, and transcribing code from paper back into something
useful was an error-prone process.
- Papers describing novel ideas in the field were incomprehensible by default,
so that the world's most established experts on the subject would need years
to decide whether a particularly cutting-edge program is meaningful or in
fact insane gibberish.
- These experts not only see nothing wrong with this picture, but in fact,
revel in symbolic obscurity and ego-driven naming, dismissing sincere
attempts at fixing these deep seated problems as meaningless taste arguments
or pointless pop culture entertainment.
If you were an experienced programmer. you would rightly call me insane.
If you were a mathematician, it would be a day ending in y.
================================================================Trying to carry the precision necessary for implementation throughout all notation quickly obscures the math beyond comprehension. Basically you're importing all the complexity that arises in programming (leaky abstractions, implementation details, etc) into math for little benefit.
For the same reason we still speak in languages full of vagaries and ambiguities instead of constructed languages: For the most part, they get the job done, and when more precision is necessary we have alternatives (legalese, mathematical notation, PL's).
For example, in the book "Structure and Interpretation of Classical Mechanics," the authors choose more precise language (scheme code) to make common misconceptions of notation clearer.