What is the meaning of proof of a proof?

Question

After reading about Curry-Howard corrsepondence and looking at some proofs written in coq i've thinked about meaning of proof of a proof.

1. We can express proofs as a computer program
2. Proof is correct when program compiles
3. 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?

Answer 1

Lewis Carroll, in 1895, recognized the infinite regress possible.

See "What the Tortoise Said to Achilles" here: http://www.ditext.com/carroll/tortoise.html