The Curry-Howard correspondence says that a program is the same as a proof. A proof of what, though? Not that the program does what it's supposed to. No matter how far you go with formal methods, what the program is supposed to do is always informally specified. (There may be a formal specification. That specification wasn't handed down from on high at Mount Sinai, though. It's a formalization of the informal, badly-stated, half-unconscious informal specification that is the impetus for creating the program. Does the formal spec match the informal one? Can you prove it? No, you can't - certainly not formally.

It's like you read the article, and set about disproving it, without ever really understanding it.