The Curry-Howard isomorphism (types are theorems, programs are proofs) | Heykuki News