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

1) nobody cares

2) it's a pretty rare skillet with specialist tooling, that doesn't really provide the itch scratch of most open source

3) "correctly formulating the problem in a formal specification" is really hard, given the inability of most stack overflow posters to formulate questions rigorously

4) for almost all projects, we value mutability over eternity

Hmm, I think at least people on HN care. I think most developers care. Did you see the recent post about the slow loading times in GTA 5?

Problems like that would go away with something like this, no? (if it is possible and there isn't a fault in my argument)

> Did you see the recent post about the slow loading times in GTA 5?

Did you? It seems pretty obvious to me that Rockstar knew that this was slow as hell, and they were showing ads during that time window. Business interests are not software engineering interests, so I don't think problems like that would go away with something like this, no.

I don't know, a lot of people in that thread argued that this must've actually cost Rockstar a lot of money. I'm not sure which side of the argument is true, both sound plausible to me.

The people who can't be bothered to play now, will demand R* do something about the cheaters and people who bought their way to the top already. The people they gained won't stay, because R* won't ditch the people who actually make them money.

So all this will really do is put more load on their servers, now that the bottleneck moved off of your hardware and back onto thiers.

No, formal verification would not help with code being accidentally quadratic due to a standard library function doing something different from what the author thought it did. The lack of a formally verified json parser is also almost certainly not why the author of the code chose to roll their own parser rather than using one the of many pre-existing libraries.

another angle is the business perspective.

a lot of software is deployed in the service of the goals of business. To serve that purpose it often isn't necessary for the software to be completely correct. If it is probably sort of correct that's often good enough. Better to have something sort of correct deployed and running next week than something that costs more money and time to build, is a lot harder to hire people to maintain, relies on a formal analysis that is highly sensitive to changes in assumptions, and achieves a level of correctness that is unnecessary for the situation.

from this perspective, investing effort into formal methods will often give a poor return on investment compared to alternatives of hacking things together & running a few tests to catch obvious defects.

In some situations it seems to be worth investing in formal methods. Eg relatively well defined systems with very high costs if they fail.

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

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

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.

Thank you, your point 5) is extremely interesting. Something clicked when I read that.

I guess what that means, right now, when we're writing Software, we're really only ever solving a small part of the whole problem. A lot of the problem space isn't even considered. (I'm saying this completely neutral btw, I don't think it's either good or bad. It's a trade-off and probably what allows us to have all the software we have now.)

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

Thank you very much for the answer!

Could you elaborate on the last (now first, after edit) point you made? Sorry if the question is naive, I don't know much about this topic. Why can't you do that?

So picture trying to take a C snippet and using it inside a JavaScript project. On top of the different language syntax, each language has different definitions on equality, strings, arrays, numbers, control flow, pointers etc. so there's no simple mapping that would let you translate the C snippet into a snippet a JavaScript interpreter would understand and if you're not careful with your mapping you're going to get bugs.

Similarly with theorem provers, on top of just the syntax, they each have their own definitions for equality, data structures etc. that don't have simple mappings, as well as differences in the basic proof axioms all proofs must be built on. Both specifications and their proofs won't map easily between theorem provers which you'll have to reconcile somehow.

Thanks for the explanation!

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.

Why not all of those? Genuine question. Sorry, my knowledge of this topic is very limited.

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.

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?

Great questions. Well off the top of my head, you could just post multiple solutions to the same problem specification. Just like you can have multiple (valid) answers to the same StackOverflow question.

That's why it would be awesome if you also added performance/memory characteristics to each solution you posted - then you could easily see which one is better for your situation.

Actually, even better - the memory/performance constraints could/should arguably be part of the problem formulation in the first place.

I guess Coq/Lean standard libraries fit this definition.

Exactly, I got this idea from a talk about Lean: https://www.youtube.com/watch?v=Dp-mQ3HxgDE

You should look at this like software development. New programming languages come out that try to solve the problems of all the previous languages and unify everyone to code and be productive in the same ecosystem...until another language comes out etc.

It's very hard to get everyone to agree how code plus mathematics should be written. There's a lot of fragmentation and ongoing attempts to unify.

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