But doesn't the constant Gödel reference push people, exactly, to work toward effective cheats? Imagine if the people putting in effort to make real systems instead spent their time trying to create the self-verifying prover.
Plus, hardly anyone is making a self-verifying prover. Someone just asked about that. I tried what I hope is the proper response of simply linking to a self-verifying prover that succeeded in that goal up to first-order logic. So, that's already done with us just needing similar ones for checkers of HOL, Coq, ACL2, etc. Contrary to your implication, the Milawa techniques are based on and supporting some of most practical verification work to ever be done. So, one of few times someone totally ignored Godel in what non-experts would consider Godel's domain led to one of best results in formal methods.
We don't need Godel at all in these discussions. We just need to explain what formal methods are, their successes, their limitations, how to properly use them, and ideas for new projects.