3 ms·
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” (ty
by zmgsabst 2y 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).
- 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".