Can Curry-Howard prove a theorem from the types in your program, that has nothing to do with your program? The following link states:


  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) -&gt; (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?
I'll answer the opposite question which is: 


  can Curry-Howard prove a theorem for your program, which has nothing to do with the type? 


The answer is yes, depending on the meaning of "nothing to do". I'll leave the Curry-Howard aspect aside somewhat, but it underlies a lot of this approach. 

The key idea is Wadlers' Theorems for Free! building on ideas from Reynolds, which allow you, given a program type, to deduce something about the program. For example, a program $f$ of type

(a, b) -&gt; (b, a)


in haskell must satify

$$ \forall x\ y,\ f\ (x, y) = (y, x)$$

and therefore be the swap function.