Comment by zmgsabst
1 month ago
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".