# An1lam's Short Form Feed

post by An1lam · 2018-08-11T18:33:15.983Z · score: 14 (3 votes) · LW · GW · 2 commentsIn light of reading Hazard's Shortform Feed [LW · GW] -- which I really enjoy -- based on Raemon's Shortform feed, I'm making my own. There be thoughts here. Hopefully, this will also get me posting more.

## 2 comments

Comments sorted by top scores.

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.)