I can understand where this is coming from, but as a PhD in Pure Math who is now a programmer, I think it is badly misleading. Many people here will speak eloquently about how wonderful proof assistants are, and how lamentable it is that modern mathematicians don't use them, but then it usually transpires that they themselves are not mathematicians, and really don't have a clue about just how free form mathematics is when practised at the highest levels.
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.
================================================================
Math is for communication between mathematicians and programming languages are ultimately compromises for the purposes of precision and the limits of computers.
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.
This list sounds like new programmers complaining about the difficulty of language syntax - which largely vanish once you know enough that it melts into the background and poses no significant cognitive burden. They are valid observations, but they miss the point that (generally speaking) mathematics is about communicating ideas to other people who speak the language. Most high level mathematics involves both a great deal of implicit knowledge, and potentially introduces completely new ideas that may not be easily expressed with existing terminology.
Yes. In general the mathematics that people bother to talk about is much, much more complicated than most programs. There is more complexity in a few words of mathematics than most programs that exist; mathematicians are drawing on thousands of years of constant labor and forward progress from the brightest people in human history with every word or symbol they write. Plus, they feel free to invent new notation to capture the creative ideas they require it for at will. If your idea isn't new enough to require new notation, it's not really difficult/creative enough to be worth writing a paper about. Mathematics is written to express ideas for other humans to read, not for machines to execute correctly to accomplish a task.
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.
That's sort of the point. We will come up with a new language when the old is no longer sufficient for the problem at hand. It's as if math is stuck using punch cards.
I found thinking in terms of Mathematica and MatLab helped me think about math syntax as it is more complete.
The syntax of any programming language is easier to grok because it is more concrete - not because it is more complete. It is not so much that "math is stuck using punch cards", but rather that you only really need as much formality as it takes to express the central idea - which is far short of what would be required for a concrete implementation.
This would have been funnier if it was even remotely true.
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.
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.
What took the longest to click for me is that there is no distinction between a variable and an array in mathematics- if you write x_i = y_i you are equating each element of two potentially infinite sets. There are implicit looping operations everywhere. Also in the equation x=2y x and y are not variables in the programming sense of the word but rather every pair of x and y that are a solution is a member of the solution set. So it's a very different approach.
Well, if you wanted to be precise you should specify for which indices x_i=y_i should hold. But if it's clear from the context then that might be left out.
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').
Yeah, the key insight I think is that if you don't put any constraints on some variable then the intent is that the equation is true for any choice of that variable- so since x_i = y_i for any i, then it's logically the same as saying x0 = y0, x1 = y1, ... It was an aha moment when I realized what they were doing there. Very elegant actually.
13 comments
[ 3.4 ms ] story [ 36.6 ms ] threadI'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:
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.
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.
I found thinking in terms of Mathematica and MatLab helped me think about math syntax as it is more complete.
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.
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').