3 ms·
As somebody with a PhD in math, I really wish that math was taught via strongly typed programming languages. There is so incredibly much low-lying work done th
by klyrs 4y ago
As somebody with a PhD in math, I really wish that math was taught via strongly typed programming languages. There is so incredibly much low-lying work done through deep layers of abstraction that it can take hours or even days to digest a short paragraph in a field adjacent to one's expertise.
Of course, that's the dream. The reality is that people are making very strong efforts at computer proofs, and the languages I've worked with in that space are highly un-ergonomic. On the other side of the chasm, calculus of types is largely relegated to category theory which is its own onion of complexity. To my awareness, Haskell is currently the sweet spot. In the hopes of being proven wrong, I'd guess that we're at least a century away from a Grand Unified Notation that allows a fluid translation between what the mathematician is thinking and how the computer can compute.
- nequo 4y agoLean 4 seems promising, too.[1] Although it looks very much like Haskell. [1] https://leanprover.github.io/functional_programming_in_lean/ https://leanprover.github.io/functional_programming_in_lean/
- klyrs 4y agoYes, progress is under way! It's been a few years since I tried to plumb these depths, it's probably time to look again. But I don't need to look to know that we're not there, where "there" means both accessible and widely adopted.
- chalst 4y agoLean is particularly exciting because of the work Kevin Buzzard has been doing in the Xena project: https://www.ma.imperial.ac.uk/~buzzard/xena/ https://www.ma.imperial.ac.uk/~buzzard/xena/ He started by getting undergraduates to tackle formalising the maths they did in Lean, and his success with this as a didactic tool has spread the idea among quite a lot if mathematicians.
- jhanschoo 4y ago> There is so incredibly much low-lying work done through deep layers of abstraction that it can take hours or even days to digest a short paragraph in a field adjacent to one's expertise. Indeed, once you start to think about formalizing a research-level proof, it brings into focus the sheer number of trivial cases and natural transformations that a standard informal proof in a paper omits.