After reading about Curry-Howard corrsepondence and looking at some proofs written in coq i've thinked about meaning of proof of a proof.
- We can express proofs as a computer program
- Proof is correct when program compiles
- We can test compiled program or even write correctness proof for it.
So, what test of a proof checks? What correctness proof of a computer-program-proof will prove? Proof correctness is ensured on compilation stage, what is the meaning of proof of a proof? Is there any meaning?