[nickbauman]

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.

[Jweb_Guru]

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.