2 ms·

> I find one of the biggest mistakes programmers have about mathematical notation is that it's somehow just a terse, badly implemented programming language. But

by User23 4y ago

> I find one of the biggest mistakes programmers have about mathematical notation is that it's somehow just a terse, badly implemented programming language. But this is a very poor understanding of what mathematical notation is doing. 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_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

Karrot_Kream 4y ago
Complete proofs and programs are isomorphic. Many proofs while incomplete are perfectly legible to experienced practitioners who can fill in the details without getting bogged down in trite steps. Morevoer, isomorphisms are simply provable facts between two types of objects. Most isomorphisms are generally used to convert one object into another object which is more amenable to being used in a given proof. An isomorphism does not beg the conversion and there are many trivial isomorphisms of limited use.
alphabetr 4y ago
I get the feeling that you're stuck in Terry Tao's 'rigourous phase' of mathematical understanding, where everything in the end is a computation and has to be carried out according to a set of rigorous steps and definitions. 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.

by User23 4y ago

Karrot_Kream 4y ago

Complete proofs and programs are isomorphic. Many proofs while incomplete are perfectly legible to experienced practitioners who can fill in the details without getting bogged down in trite steps. Morevoer, isomorphisms are simply provable facts between two types of objects. Most isomorphisms are generally used to convert one object into another object which is more amenable to being used in a given proof. An isomorphism does not beg the conversion and there are many trivial isomorphisms of limited use.

alphabetr 4y ago

I get the feeling that you're stuck in Terry Tao's 'rigourous phase' of mathematical understanding, where everything in the end is a computation and has to be carried out according to a set of rigorous steps and definitions. 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.