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.