Comment by vector_spaces
1 month 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)
https://www.landsburg.com/grothendieck/mclarty1.pdf
That'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.
If 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.
1 reply →
Literally 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).
No, it is not the same, CH is just a particular instance of it, much like "shape" is not the same thing as "triangle".