3 ms·
The chains of reasoning are only long and intricate if you trace each result back to axiomatics. Most meaningful results are made up of a handful of higher-leve
by vector_spaces 2y ago
The chains of reasoning are only long and intricate if you trace each result back to axiomatics. Most meaningful results are made up of a handful of higher-level building blocks -- similar to how software is crafted out of modules rather than implementing low-level functionality from scratch each time (yes, similar but also quite different)
- Koshkin 2y agohttps://www.landsburg.com/grothendieck/mclarty1.pdf https://www.landsburg.com/grothendieck/mclarty1.pdf
- seanhunter 2y agoThat's a fantastic essay - I feel like it's the tip of a rich vein that I'm looking forward to exploring. Thanks for drawing it to my attention. I can't wait to get on to studying abstract algebra and categories properly for myself which is probably about a year off at this point.
- xanderlewis 2y agoIf you want to study categories from a relatively foundational point of view, the author, McLarty, also has a very readable book called Elementary Categories, Elementary Toposes.
- seanhunter 2y agoSounds perfect. Thank you very much for the tip.
- zmgsabst 2y agoLiterally the same: A type is a theorem and its implementation a proof, if you believe that Curry-Howard stuff. We “prove” (implement) advanced “theorems” (types) using already “proven” (implemented) bodies of work rather than return to “axioms” (machine code).
- practal 2y agoNo, it is not the same, CH is just a particular instance of it, much like "shape" is not the same thing as "triangle".