Hacker News new | ask | show | jobs
by Jweb_Guru 3120 days ago
> Formal proof of behavior is hard and probably specious.

Utter nonsense. Formal proofs are specious because you can't do a formal proof of problems that are so ill-defined, we don't even have algorithms that solve them in enough cases to be road-safe yet? If you restrict your focus to software that actually exists, almost all of it is amenable to formal modeling.
1 comments
nickbauman 3118 days ago
You're making a philosophical argument about problem definition being the reason why we can't use formal proofs for many common sense problems. I wish you the best of luck.

My claim is that proving that software is correct using formal logical proofs is tautologically specious unless you extend the software to the problem it's trying to solve. Once those problems are of sufficient complexity (or interest, I might add), logic fails.

link
Jweb_Guru 3117 days ago
A best-in-class, hard-real-time, preemptible operating system has been formally verified (along with many other components). CompCert exists. Iris progresses apace. Every day, newer and more complex formal systems are proved correct. I don't really buy the "logic fails at sufficient complexity" argument. By all accounts, it's succeeded where people have put in the effort.
link