[lomnakkus]

While this is a fun aphorism, it's getting less and less applicable these days since many proof systems (and programming languages that double as such) allow for code extraction to e.g. ML or C code. Naturally, the usual caveats apply: You'll want proof that the code extractor is correct. (But then, you'd want proof that the proof system itself is correct, regardless.)

Nevertheless, the aphorism is part of the reason that I'm (also) sceptical of using proof systems that don't allow for code extraction. Assuming you're actually trying to prove things about programs and just just proving things for e.g. math.

[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.)