Hacker News new | past | comments | ask | show | jobs | submit login
The Teetering Towers of Abstraction (bit-player.org)
58 points by alberto_ol on Jan 22, 2020 | hide | past | favorite | 4 comments



Modern mathematics is based on formal systems, not an "abstraction" of counting jelly beans. That's like saying that chess is an abstraction of war. It seems like a reasonable analogy but they're actually entirely different things.

A formal system of category theory is no more abstract than a formal system of natural numbers. The apparent difference in abstraction is relative to the subjective (and irrelevant) choice of application. Category theory seems abstract for counting jelly beans, but for other applications it might be less of an abstraction than arithmetic.

https://math.stackexchange.com/questions/298912/real-world-a...

Similar to how computer programs can be broken down into physical laws about the movement of electrons, mathematical proofs can be broken down into deductive statements about ZFC set theory, etc. In both cases this is ideally about concretely building upon previous work, not creating abstractions.

The problem of incomprehensible proofs isn't about a "tower of abstraction". There's no abstraction within formal systems. The system is described and the implications are deduced. The problem is expanding complexity with a lack of detail and exposition that allows for misunderstandings and perhaps even errors.


>The problem is expanding complexity with a lack of detail and exposition that allows for misunderstandings and perhaps even errors.

I think this is also a problem in modern software development. Everyone writes a new API; uses obscure library A,B, and C; throws things together and claims it's their new pattern X.

Then you're left with all this new complexity introduced by custom abstractions that often aren't transferable from one development case to the next and require learning entirely new sets of concepts that are poorly explained.


I think mathematicians favour abstractions more then programmers, opposite as to what the OP suggests

Its like when you're coding this solution in haskell and start to wonder if the GHC is going to optimize all the intermediary data structures with it's di-forestation algorithms as apposed to doing it in a imperative language and including an assembly file with the floating point routines implemented using SSE instruction.


Whoa.




Consider applying for YC's Summer 2025 batch! Applications are open till May 13

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: