I think this error in thinking comes from the fact that Sigma notation can often be trivially implemented as a for loop.
Programming languages are designed to describe a specific computation, whereas mathematical notation is typically trying to describe an idea (one that might not even have a implementation!) Notation only sometimes and coincidentally describes computation as well.
The ambiguity, implied variables etc are an essential part of mathematical notation in the same way it is in common spoken language. Mathematical notation exists to help abstract and work out very hairy ideas, and often that ambiguity is necessary to show connections.
> code should be optimized for readability, not writtability
Mathematical notation is readable if you're literate in it. It takes lots of practice to become fluent in it, but once you become more familiar it's much easier to read than text (which is why it's used in the first place). Mathematical notation is an extension of mathematical writing, not computational implementation.
Reading mathematical notation is much closer to reading poetry than reading code.
No, we think that because proofs and programs are isomorphic[1]. It's not a mistake: traditional mathematical notation provably is a terse badly implemented programming language. Actually it's worse than that, because oftentimes it doesn't even parse. Now I'm not going to say I can't on some level see the appeal. After all I think Perl is a lot of fun to code in.
Naturally, its adherents are practiced at making a virtue out of its defects. Who wants to admit they dedicated considerable brainpower to doing something in a fundamentally suboptimal way? That doesn't really matter though. As Mathematica and other tooling shows, the formalists have already won and now it's just a matter of mopping up the stragglers, or waiting for them to age out. This isn't terribly surprising to those who know the basics of the history of mathematics. It took something on the order of two centuries before Recorde's innovation of the equal sign was generally accepted.
[1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
I get that, but it does miss a bit the cultural context of how mathematically fluent people use mathematics to communicate with each other. When you're discussing maths with colleagues in front of a blackboard, you're often not really trying to prove anything, but discussing the relationship between mathematical objects. In this context the ambiguity and implication in the notation is almost a requirement, otherwise the communication speed tanks.
Having a mathematical discussion between a group of people all fluent in the context and terminology is a wonderfully fluid thing.
I was so accustomed to hearing that mathematics is nothing if not rigorous, but the more I reflect, mathematics is much more dependent on social convention and agreement amongst a community. While an outsider might think that proofs rigorously establish theorems, the purpose of a proof might be better seen as having enough detail to convince a substantial portion of the prominent mathematicians in a field that the proof is correct. In fact, there are theorems (e.g. the ABC conjecture) where a “proof” has been proposed, but not enough mathematicians have expertise with the techniques used to prove it in order to agree whether the proof is sufficient or not (though I’ve heard that the general opinion is that the proof does not suffice). William Thurston wrote one of my favorite essays related to this topic: https://www.math.toronto.edu/mccann/199/thurston.pdf
Reflecting on my own experience in mathematics, a better way to think of proofs is as being composed of “thought patterns” which many mathematicians agree are likely to be correct - when I scan a proof, I don’t look through every detail to verify that it is correct, but rather run it through a series of high level tests to see if it fails in any way, then if it passes all of those I look more closely at the argument and analyze the structure and mathematical power of each statement (e.g. one is unlikely to establish a hard analytic result through purely algebraic means, so where is the magic going on?) and so on until I’ve convinced myself that the argument is probably true. Other times, the result may be “visually apparent” (e.g. in geometry) at which point it might be sufficient for me to just to connect certain canonical arguments with the pictures as I read through the proof. For an excellent overview of this process, read Terry Tao’s blog on identifying errors in proofs : https://terrytao.wordpress.com/advice-on-writing-papers/on-l....
I don’t feel as confident commenting on the programming/computational perspective, as I’ve probably developed a very idiosyncratic way of thinking from approaching the topic so late in my education, but my feeling is that they are much different, and that the types of things a mathematician wants to convey to another mathematician rely much more on “trust” rather than the kind of rigor that might be needed by a computer.
I think this would be an interesting topic to explore in longer form.
[1] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD13xx/E...
By and large mathematics education has missed the point of invention of computers. It is only occasionally used to make a point. We should be teaching mathematics with a programming first approach: get your function code to compile, ponder on its signature, write some test cases to really understand what is going on.
This just isn't true, at least in terms of developing new mathematical ideas. There are already tools (e.g Coq) for providing mathematical syntax checking etc, but nobody uses these in developing new ideas because it would cripple the process of doing mathematics.
Particularly in the early stages of work, mathematics is very intuition and heuristic driven, you tend to sketch out an idea by actively using the ambiguity in the notation. Once you've got something that looks broadly correct you progressively try to shore it up by using more detailed and rigorous argument.
Maybe as an analogy, think of how architects design houses. They don't start by placing each brick according to correct civil engineering practice. They design something that broadly makes sense and then the civil engineers 'shore it up'.
Coq isn't about mathematical syntax checking. Coq is about encoding the whole proof in such a way Coq can machine verify it. That's 100 steps further then what I'm talking about. Just a simple syntactic check. Similar to what gofmt does. Is what you are writing considered valid syntax. Not whether what you are writing is correct.
Sussman (who wrote the famous SICP book) wrote another book structure and interpretation of classical mechanics. Tough book to go through. But they start with the same premise: mathematical notation is confusing (and hand wavy at times). A better symbolic notation should reveal enough details to be able to code up the mathematics in a program. I found this approach to be bang on target, but could never get enough time to actually go through the book.
And I realised why the 'let us build it up from scratch' books work. They force you to think about the function signatures and shape of objects passed to each function. This approach reveals gaps in our understanding much better. For example, F=ma is looks like an algebraic statement, hiding the fact that `a` on the right is about time evolution of the system through the derivative.
Steven Strogatz made a funny quote in his infinite powers book. (I'm paraphrasing), if Newton was doing this in today's era he might create a flipbook animation to make this point and not symbols.
Another great book on this topic is "History of Mathematical Notations" https://www.amazon.com/History-Mathematical-Notations-Dover-...