I’ve recently been obsessing over the idea of trying to “make math more like programming”. I’m not sure if it’s just because I feel fluent at programming and still not very fluent at abstract math or also because programming really does have a feedback loop that you don’t get in math.
Regardless, based on my reading it seems like there’s a general consensus in math that even the most modern theorem provers, like Lean and Coq, are much less efficient than typical “informal” math reasoning. That said, I wonder if this ignores some of the benefits that programmers get from writing in a formal language, i.e. automatic refactoring tools, fast feedback loops, and code analysis/search tools. Also, it seems like a sufficiently user-friendly math theorem proving tool could be useful for education. If kids can learn how to program in Javascript, I have to believe they can learn to prove theorems, even if the learning curve’s relatively steep.
Maybe once I play around with Lean more, I’ll change my mind, but for now, I’m sticking to my contrarian viewpoint.
There’s a difference between solving a problem where you’re 1) trying to figure out what to do. 2) Executing an algorithm. 3) Evaluating a closed form solution (Plugging the values into the equation, performing the operations, and seeing what the number is.)***
Names. If you’re writing a program, and you decide to give things (including functions/methods) names like the letters of the alphabet it’s hard for other people to understand what you’re doing. Including future you. As a math enthusiast I see the benefit of not having to generate names*, but teaching wise? I can see some benefits of merging/mixing. (What’s sigma notation? It’s a for loop.)
Functions. You can say f’ is the derivative of f. Or you can get into the fact that there are functions** that take other functions as arguments. You can focus narrowly on functions of one-variable. Or you can notice that + is a function that takes two numbers (just like *, /, ^).
*Like when your idea of what you’re doing /with something changes as you go and there’s no refactoring tool on paper to change the names all at the last minute. (Though paper feels pretty nice to work with. That technology is really ergonomic.)
**And that the word function has more than one meaning. There’s a bit of a difference between a way of calculating something and a lookup table.
***Also, seeing how things generalize can be easier with tools that can automatically check if the changes you’ve made have broken what you were making. (Writing tests.)
I’ve recently been obsessing over the idea of trying to “make math more like programming”. I’m not sure if it’s just because I feel fluent at programming and still not very fluent at abstract math or also because programming really does have a feedback loop that you don’t get in math.
Regardless, based on my reading it seems like there’s a general consensus in math that even the most modern theorem provers, like Lean and Coq, are much less efficient than typical “informal” math reasoning. That said, I wonder if this ignores some of the benefits that programmers get from writing in a formal language, i.e. automatic refactoring tools, fast feedback loops, and code analysis/search tools. Also, it seems like a sufficiently user-friendly math theorem proving tool could be useful for education. If kids can learn how to program in Javascript, I have to believe they can learn to prove theorems, even if the learning curve’s relatively steep.
Maybe once I play around with Lean more, I’ll change my mind, but for now, I’m sticking to my contrarian viewpoint.
It seems like a useful idea on a lot of levels.
There’s a difference between solving a problem where you’re 1) trying to figure out what to do. 2) Executing an algorithm. 3) Evaluating a closed form solution (Plugging the values into the equation, performing the operations, and seeing what the number is.)***
Names. If you’re writing a program, and you decide to give things (including functions/methods) names like the letters of the alphabet it’s hard for other people to understand what you’re doing. Including future you. As a math enthusiast I see the benefit of not having to generate names*, but teaching wise? I can see some benefits of merging/mixing. (What’s sigma notation? It’s a for loop.)
Functions. You can say f’ is the derivative of f. Or you can get into the fact that there are functions** that take other functions as arguments. You can focus narrowly on functions of one-variable. Or you can notice that + is a function that takes two numbers (just like *, /, ^).
*Like when your idea of what you’re doing /with something changes as you go and there’s no refactoring tool on paper to change the names all at the last minute. (Though paper feels pretty nice to work with. That technology is really ergonomic.)
**And that the word function has more than one meaning. There’s a bit of a difference between a way of calculating something and a lookup table.
***Also, seeing how things generalize can be easier with tools that can automatically check if the changes you’ve made have broken what you were making. (Writing tests.)