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.
My question is: Can Howard-Curry prove a theorem from the types in your program, that has nothing to do with your program?