DEV Community

Discussion on: A Gentle Introduction to Curry-Howard Isomorphism

j3698 profile image

Wow thanks! Question, for programs like "factorial", or"add", these are all proofs of nat -> nat. Are these at all useful? I would think inherent in the structure is proof of something, but I can't see what.