[roca]

You don't need to prove that the proof system is correct. It suffices to extract a proof of the properties you care about for the particular program you care about, and then check that that particular proof is correct. This can generally be done with a very simple proof-checker whose own correctness can fairly easily be checked by hand.

[lomnakkus]

True, but that adds an extra burden for programmers... and if proof systems are ever going to gain widespread acceptance (that'll be the day!), the ergonomics of using them need to be improved. (That is, having an extra manual step is not acceptable.)