In the context of the Curry-Howard isomorphism you don't "prove things about programs".
Programs ARE proofs. Not all programs, mind you. You need to be using a dependently-typed language like Agda, Coq or Idris.
The link in my post to the UniMath project is a bunch of codified proofs to various theorems in Category theory, Topology, Combinatorics etc.
Sure, programs are proofs in the context of Curry-Howard. But not necessarily proofs of what you want them to prove.
It may be an a-priori truth in the context of the particular proof you are working on, but a-priori your theorem there is always an axiom.
Wanting to prove that X is a theorem of a-priori truth Y is the same thing as writing the algorithm for f: Y -> X
A proposition is a type. Writing the algorithm which implements the type is the same as proving it.