You either misunderstood or misstated the Curry-Howard isomorphism. Types correspond to _propositions_, programs themselves correspond to proofs. Now, that is

You either misunderstood or misstated the Curry-Howard isomorphism. Types correspond to _propositions_, programs themselves correspond to proofs. Now, that is one hell of a correspondence and I don’t mean to downplay it at all. But the reason why this isn’t practical in daily programming is that a type represents a set, so all that the isomorphism gets you is knowing that given a member of one type as input you get a member of another type as the output. _Any_ member. This is the problem - the difficulty in verifying logic is showing that the correct output _value_ is given for all input values. Trust me, I have played with Coq for quite a while. Realizing this is what made me abandon the belief that types are some kind of savior. They can be useful, but the program (or proof) itself is what is difficult to get right. I rarely return the wrong type from a function.