Why aren't we building a database of formally verified software?

Question

Where is the flaw in the following argument?You can formally verify software/algorithms for correctness, but formal verification is difficult and takes a long time.So why can't we do it in piecemeal? Imagine something like StackOverflow, but instead of posting a question, you post a formal specification. The answers to your post are then formally verified pieces of software.The advantage of this approach would be that the results would be useful forever. Right now we're always building on foundations of sand, because we can never really be sure that our algorithms are correct/optimal.You could then go even further and connect the verified algorithms/components from this hypothetical StackOverflow. So instead of posting a new formally verified algorithm, you piece it together with parts that have been individually formally verified. That way you only have to verify the new additions.This way we could build a database/repository of "eternal" software. Eternal in the sense that once a problem is solved, it's like a mathematical proof, it's solved forever (as long as the verification was performed correctly).You could even add more things to the verification step, like performance analysis - that way we could immediately tell for each of these algorithms/components, how fast they perform.This of course wouldn't solve software development - instead it would shift the challenge to correctly formulating the problem in a formal specification.Is this possible? If so, why isn't this being done?

pjc50 · Accepted Answer

1) nobody cares2) it's a pretty rare skillet with specialist tooling, that doesn't really provide the itch scratch of most open source3) "correctly formulating the problem in a formal specification" is really hard, given the inability of most stack overflow posters to formulate questions rigorously4) for almost all projects, we value mutability over eternity

Taikonerd · Answer

Here's an article that touches on some of the points that the other commenters are bringing up: "Why Don't People Use Formal Methods?"[0]
Excerpt: "The incredible progress here is evident in the IronFleet project: by using advanced SMT solvers and a cutting-edge verification language, Microsoft was able to write 5,000 lines of verified Dafny code in only 3.7 person-years! That’s a blazing-fast rate of four whole lines a day."
[0] https://hillelwayne.com/post/why-dont-people-use-formal-meth...

zero_deg_kevin · Answer

I think some of the "why" has to do with it being time-consuming and expensive. There's also the "hur-hur n00b, your spec can be wrong, so verification is pointless" crowd that pops up any time the subject comes up.That said, my favorite verified software packages are seL4 (https://sel4.systems) and the CompCert C Compiler (https://compcert.org/compcert-C.html).

l0b0 · Answer

In addition to pjc50's answer:5) Right now it's probably harder (in most cases) to write a correct formal spec than actually implementing that spec. Otherwise formal specs would be much more popular in general.6) The proportion of software which is actually algorithmically interesting these days is tiny. I expect something like 99%-99.999% of lines of code are basically stuff that's been done a thousand times before.

seanwilson · Answer

- It's like asking why can't we connect together all software ever written so each software problem only needs to be coded once. Ideally you could, but you can't. The same way there's different programming languages (with major and subtle differences), different libraries that do similar things, different APIs, different data structures etc. all attempting to improve on something, formal verification has competing languages, logics, tools etc. You can't just take a PHP library and use it as if it was a JavaScript library, the same way you can't take a proof in Isabelle and use it in a Coq proof.
- Correctness proofs of even simple algorithms can be research grade problems that take several person years of effort from (hard to find) experts, so you're not likely to get casual Stack Overflow style contributions because of the order of magnitude difference in time and expertise required.
- The time required to verify correct software will come at a major cost to other factors like features and speed. I don't think 100% correctness is a driving factor for many domains like web servers, browsers and IDEs, so your database of correct software isn't going to be widely used until it catches up on other factors.

potiuper · Answer

Formal verification of what? Termination? Memory-leaks? Undefined Behavior? Formal verification without qualification is about as meaningless as corporate jargon; with qualification it is not formal verification anymore. Formal verification requires a formal specification that is based on a mathematical model of a system. Those models and the methods used to define them alone are effectively infinite.

nonameiguess · Answer

A lot of the software that has been formally verified is either proprietary, classified, or used for academic research. Historically not the most open of communities.

whycombagator · Answer

I think the biggest hurdle to a piece of software like this would be what database technology to use. /s
In all seriousness, the idea is very interesting.
I haven’t given this much thought, and maybe I don’t fully understand the proposed idea, but how would you deal with improvements/advancement to already solved things? Like when the fenwick tree was invented
Or how do you deal with competing solutions to a problem like quicksort vs mergesort?

hirple · Answer

I guess Coq/Lean standard libraries fit this definition.

nawgz · Answer

I mean, isn't the answer clear? It might be slick and theoretically beautiful, but no entrepreneur has managed to convince any portion of industry that it's worth money, so therefore no one pursues it