[vector_spaces]

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]

https://www.landsburg.com/grothendieck/mclarty1.pdf

[seanhunter]

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.

[xanderlewis]

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.

[seanhunter]

Sounds perfect. Thank you very much for the tip.

[zmgsabst]

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).

[practal]

No, it is not the same, CH is just a particular instance of it, much like "shape" is not the same thing as "triangle".