[nickbauman]

Formal proof of behavior is hard and probably specious.

There cannot be a formally logical explication of code for even "common sense problems", like, say, how to safely drive a car. It doesn't exist because it's probably impossible but it's at least not feasible. Instead we use sampling of real world data to train models to solve this problem. This is the story of Data over Logic.

[pron]

Most software is very different from one that drives cars, but even in that case, while a complete specification (i.e., one that fully describes what driving a car safely is) is very hard, you can still quite easily specify many very useful correctness conditions. For example, you could state that the car must never go on the sidewalk or move to oncoming traffic unless it's trying to avoid some accident; similarly for running a red light, going over a crosswalk while there are pedestrians on it, or going over 100MPH. Verifying each of those would make your program safer, and that's the goal of formal methods -- not to make the program perfect, but better.

A complete formal specification of simpler programs or program components -- say banking systems or specific controllers in the car -- are not only possible and feasible but actually used in practice. A good number (I don't know if it's the majority or not) of avionics programs are formally specified and verified (although normally using model checkers rather than proofs). Having said that, different kinds of software can benefit from formal methods to different degrees. I'd say that if you can write tests for it, then you can write at least partial specs for it, too, but whether or not doing so is worth it varies by circumstance (in the cases I've used formal methods recently, it was not for more correctness but actually because it was cheaper than tests).

Also, we must separate formal specification from formal proof. Formal specification means writing what the program must or must not do in some precise formal language. Formal proof is one of many forms of verifying that specification. It provides the most confidence, but it is also by far the most expensive. Most programs can benefit greatly from formal specifications but can settle for weaker, but far cheaper, forms of verifying them.

[Jweb_Guru]

> 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.

[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.