This is very vague about what Curry-Howard means. Curry-Howard means that any type can be interpreted as a theorem in some logical system, and any term can be i

This is very vague about what Curry-Howard means. Curry-Howard means that any type can be interpreted as a theorem in some logical system, and any term can be interpreted as a proof of its type. This does not mean that those theorems have anything to do with your program. Take the following function: swap : forall a,b. (a,b) -> (b,a) swap pair = (snd pair, fst pair) The type here is forall a,b. (a,b) -> (b,a). The logical meaning of this type is (a and b) => (b and a). Note that this is a theorem in logic, not a theorem about your program. This is entirely different than what the types say about your program. Those properties you get from progress/preservation proofs of the type system. Now it is certainly the case that in dependently typed languages you can get the logic from Curry-Howard to express theorems about values in your program. That's the whole point of dependent typing. But it's important to to keep in mind that statements such as this: > Look again at the OCaml Set module example above. You already get a universally-quantified property just from using the type system to guarantee an invariant expressed in an ADT. That’s the import of the Curry-Howard Isomorphism, minus any appeals to more expressively powerful type systems. are nonsense. The fact that the module enforces the property P(n) === S1.mem n (S1.singleton n) = true Q(n) === forall m \in int. m /= n -> S1.mem m (S1.singleton n) = false has nothing to do with Curry-Howard. Which proves Kell's point about the equivocation around type theory.