alt Hacker News> proofs for proofs.
What does that even mean? Sorry, this is just a nonsensical term.
The issue is not that the proofs could be wrong. It's that humans don't understand them even if they are verifibly correct.
In contrast, with software you don't know if it's correct. That's what you have a test for. Even if you understand it, there could be a bug. And tests could have bugs too, so you can have tests for tests. But proofs that are verified are correct. That's it.
Imagine you have a program that is formally proved to be correct. You don't need a test for it. However you might not understand it. Having a test or not does not change that.
TL;DR: Correctness and understandability are (mostly) independent properties.
Replies
jdw64 • today at 7:39 AM
[dead]
Thank you for spelling this in detail!
One thing I might add is that not all programs can be proved to be correct for the simple reason that not all purposes of a program can be mathematically specified. For example, for (even "closed world" domain programs like) a chess engine, the one thing that matters (in the absence of a complete solution of a game like there exists in checkers) is "can beat world champions", which can only be tested empirically. Or sometimes, e.g. business logic software, the purpose can be mathematically specified but not in a simpler way than the code itself.