Semantics of "Proof" are complicated. Is incorrect proof still a "proof", just one which is incorrect? If Curry-Howard holds then programs are "proofs". To w

Semantics of "Proof" are complicated. Is incorrect proof still a "proof", just one which is incorrect? If Curry-Howard holds then programs are "proofs". To write a proof is to write a program. But what about a program that has a bug in it? We say it is an incorrect program. But we still call it a program. By the same logic an incorrect proof is still a "proof" as well. And typically it is a proof - of something. Every formally valid proof proves SOMETHING, right? Instead of asking "Is this proof correct?" we should ask: "Does this proof prove what we claim it proves, or something else"?