Naturals in set theory LOL. Look ma, no abstraction boundary!
I don’t know if that changes the conclusion, but it’s worth exploiting the availability bias: pointing to that example and asking again if math feels clean.
Conversation
See the _tends to_ above, and the hedging: of course there is going to be some selection bias due to the kinds of maths I know more about. If I were a differential equations person, I think I'd have other things to say. :)
2
I’m not pushing a thesis, just sincerely curious. And mathematicians do have abstraction boundaries in practice, even when they’re not part of their formal language.
2
2
It just seems very hard to refactor mathematics. So much relies on stuff in people's head - seems very hard to change things lower down the stack – do people ever bother? (Univalent foundations?) But then, we are fighting similar battles in software… and without any proofs… 🤪
1
Wait what do you think logicians and type theorists and some category theorists have spent their time doing if not refactoring foundations? HoTT is just one of the most visible attempts (not sure how much by merit or by marketing, but it's closer to critical mass).
2
2
Yeah, might be disproportionate - thanks for the clarification. How well has the refactoring work that logicians and category theorists have done tended to permeate out to other mathematical fields?
1
1
People have compared advantages and costs, so they decided to not waste their time and shrugged. That's why mechanized proving might be a game changer (and I don't think it'll replace pen-and-paper proofs, just supplement it, but much more often than today).
1
Yup, I guess it's kind of like how it still pays for digital artists, architects, and graphic designers to draw and sketch their ideas?
1
1
Seems like it's taken a lot longer for us to get to the stage where computer aided theorem proving is something that most folks *want* to use, compared with say, computer graphics. And there will still be hold-outs who prefer the traditional approach, but that's fine!
1
1
Because it’s still often computer-hindered, by both accidental and essential complexity? But it is indeed getting better.
1
2
Seems like a weird problem that requires lots of interest in UX and also a deep appreciation of abstract theoretical problems. Also seems to require a ton of investment to reach parity with traditional methods - sort of second system syndrome at a massive scale I guess.
Designers of the Lean theorem prover are aiming for Microsoft-level tool support in IDEs, so we’ve basically already won even though it’ll take 20 years to get there.
1
2
Sadly, I realized this when looking up why (parts of) Lean are written in _C++_, and part of the answer was better interoperability with everything else you need for tooling.
But I had to admit they had a point, even though it runs counter against all my biases.