3 ms·
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 in
by simondedalus 10y ago
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.
- nickpsecurity 10y agoNo it distracts people by making them think some legend in math showed verification was provably a waste of time. The number that show up to keep saying it on reputable forums like this one leads to increased belief it's true via repetition effect. So, it's overall bad vs mentioning something relevant to practical verifications. 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.