4 ms·
Ask HN: Why aren't we building a database of formally verified software?
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?
- nawgz 6y agoI 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
- pjc50 6y ago1) 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
- cloogshicer 6y agoHmm, 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)
- nawgz 6y ago> 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.
- cloogshicer 6y agoI 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.
- Aeronwen 6y agoThe 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.
- plorkyeran 6y agoNo, 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.
- hirple 6y agoI guess Coq/Lean standard libraries fit this definition.
- cloogshicer 6y agoExactly, I got this idea from a talk about Lean: https://www.youtube.com/watch?v=Dp-mQ3HxgDE https://www.youtube.com/watch?v=Dp-mQ3HxgDE
- seanwilson 6y agoYou 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.
- whycombagator 6y agoI 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?
- cloogshicer 6y agoGreat 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.
- deleted 6y ago[deleted]
- zero_deg_kevin 6y agoI 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 https://sel4.systems) and the CompCert C Compiler (https://compcert.org/compcert-C.html https://compcert.org/compcert-C.html).
- potiuper 6y agoFormal 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.
- cloogshicer 6y agoWhy not all of those? Genuine question. Sorry, my knowledge of this topic is very limited.
- nonameiguess 6y agoA 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.
- seanwilson 6y ago- 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.
- cloogshicer 6y agoThank 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?
- seanwilson 6y agoSo 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.
- l0b0 6y agoIn 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.
- cloogshicer 6y agoThank 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.)
- Taikonerd 6y agoHere'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-methods/ https://hillelwayne.com/post/why-dont-people-use-formal-meth...