But perhaps as we delve deeper we'll discover we're actually living in the abandoned legacy simulation project, with a terrible train-wreck of logical foundations that we can never reconcile to arrive at any coherent model of anything… 😱🤖
Conversation
The amount of "hackiness" is different per-field; does analysis have more than algebra?
But mathematical hackery, when it permeates disciplines, tends to have a quality closer to people taking care to write cache-aware code than "that function throws errors on string inputs"
1
3
You can black-box a lot of things in a way that leaves the exterior ripe for being fitted into a hole in a large, sensical structure. Maths feels like it leaks less implementation details than most things.
1
1
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.
1
1
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?
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
Show replies