3 ms·

> You cannot write one in fewer than a few MLOCs. Same goes for a modern operating system, or for an organizational software. It's always easy to say that about

> You cannot write one in fewer than a few MLOCs. Same goes for a modern operating system, or for an organizational software. It's always easy to say that about problem domains you're not familiar with. Split it into several programs that can be verified independently. > In order to keep the proof feasible, they couldn't just write any code they wanted, but were restricted to using only the simplest algorithms ("braindead simple" he called them). Frankly, I can only see this as a good thing. > but there are results in computational complexity that mean this would be pretty much unattainable for most real software (even proofs of propositional calculus grow exponentially). This comes from the assumption that you first develop the system to be verified and only then verify it. > I don't think you realize how small is the set of software that can be written in this way. As if more software were automatically a good thing.

pron 10y ago
> Split it into several programs that can be verified independently. Doesn't help if the correctness of the whole program relies on an interaction of the component. See my blog post on the matter (the complexity of verifying a composition of k components is not only exponential in the number of components, but in the complexity of each; in other words, internal complexity cannot be hidden; this was proven in 2005 I think, by noting that the interaction of k finite-state-machines can simulate a nondeterministic Turing machine with a tape of size k). > Frankly, I can only see this as a good thing. Many of the algorithms that drive most progress in verification itself -- such as SAT solving and static analysis -- would themselves fall far short of this bar. Ironically, forgoing complex algorithms altogether would make verification even harder. > This comes from the assumption that you first develop the system to be verified and only then verify it. No, the two problems are of the same complexity. Developing a correct program can be no easier than verifying one. See my post. > As if more software were automatically a good thing. Well, that's a whole other discussion. In this one, I do not attempt to judge whether software is good or bad.
- catnaroek 10y ago
  > the complexity of verifying a composition of k components is not only exponential in the number of components You're assuming that the components are allowed to interact with each other in arbitrarily complicated ways. IMO, if the complexity arises from the interaction between components, rather than staying confined within each individual component, you effectively still have one gigantic ball of mud. > Many of the algorithms that drive most progress in verification itself -- such as SAT solving and static analysis -- would themselves fall far short of this bar. Indeed. That's precisely why I'm not interested in mechanical verification anymore. > Ironically, forgoing complex algorithms altogether would make verification even harder. Perhaps. But it would also provide an incentive for exploring how much systems can be simplified. Maybe there are hard limits, but I don't think we're anywhere near reaching them. > Developing a correct program can be no easier than verifying one. The difficulty lies elsewhere: in the extremely low probability that an unverified program will be correct.
  - pron 10y ago
    > You're assuming that the components are allowed to interact with each other in arbitrarily complicated ways. Look, you can talk about worst-case (i.e. general or arbitrary) and you can talk about best-case. If you read my blog post you'll see that real-world software has been found to hit worst-case verification complexity, but neither worst-case nor best-case is what we really want. We're interested in the common case, which requires years of empirical observation. While it is certainly possible that we'll slowly be able to improve formal verification for the common case (as an industry user of formal methods, I certainly hope so and believe it will happen in a few decades), there is no current indication that this would ever be affordable. Currently, proof of correctness of anything larger than a few hundreds or a couple of thousands LOC is simply out of reach for the foreseeable future. So I'm not assuming anything, just stating the worst-case, and noting that there is no empirical indication that the common case is significantly better. > That's precisely why I'm not interested in mechanical verification anymore. Well, that's the only approach that has been shown to work in practice on real world software so far -- and they work very well (although, again, not quite in the way people who have not had experience with formal methods think). Deductive proofs (with Isabelle, PVS, Coq etc.) is used only to tie together results of automated methods, or fill in the holes where automated methods have failed. Doing it any other way is simply not economical. Even the most avid supporters of manual verification (who've actually tried it on nontrivial software) would agree. I don't think anyone believes that "ordinary" non-high-assurance real software (aside from certain very small core components) would be verified by deductive proof any time in the next few decades. The only people who believe otherwise are those who haven't actually tried formal methods on real-world software. > The difficulty lies elsewhere: in the extremely low probability that an unverified program will be correct. But software requirements aren't for 100% confidence in correctness, if only because you don't get anywhere near that with the hardware the software is running on. So the question is precisely how much more correct a software is with increasing verification effort. Like I said, there appears to be a pretty steep curve of diminishing returns. End-to-end verification is almost never affordable, but it is also almost never required. What the formal methods community is really interested in these days is how to reduce the cost of verification required to achieve current (and near-future) correctness requirements.

pron 10y ago

> Split it into several programs that can be verified independently. Doesn't help if the correctness of the whole program relies on an interaction of the component. See my blog post on the matter (the complexity of verifying a composition of k components is not only exponential in the number of components, but in the complexity of each; in other words, internal complexity cannot be hidden; this was proven in 2005 I think, by noting that the interaction of k finite-state-machines can simulate a nondeterministic Turing machine with a tape of size k). > Frankly, I can only see this as a good thing. Many of the algorithms that drive most progress in verification itself -- such as SAT solving and static analysis -- would themselves fall far short of this bar. Ironically, forgoing complex algorithms altogether would make verification even harder. > This comes from the assumption that you first develop the system to be verified and only then verify it. No, the two problems are of the same complexity. Developing a correct program can be no easier than verifying one. See my post. > As if more software were automatically a good thing. Well, that's a whole other discussion. In this one, I do not attempt to judge whether software is good or bad.

catnaroek 10y ago
> the complexity of verifying a composition of k components is not only exponential in the number of components You're assuming that the components are allowed to interact with each other in arbitrarily complicated ways. IMO, if the complexity arises from the interaction between components, rather than staying confined within each individual component, you effectively still have one gigantic ball of mud. > Many of the algorithms that drive most progress in verification itself -- such as SAT solving and static analysis -- would themselves fall far short of this bar. Indeed. That's precisely why I'm not interested in mechanical verification anymore. > Ironically, forgoing complex algorithms altogether would make verification even harder. Perhaps. But it would also provide an incentive for exploring how much systems can be simplified. Maybe there are hard limits, but I don't think we're anywhere near reaching them. > Developing a correct program can be no easier than verifying one. The difficulty lies elsewhere: in the extremely low probability that an unverified program will be correct.
- pron 10y ago
  > You're assuming that the components are allowed to interact with each other in arbitrarily complicated ways. Look, you can talk about worst-case (i.e. general or arbitrary) and you can talk about best-case. If you read my blog post you'll see that real-world software has been found to hit worst-case verification complexity, but neither worst-case nor best-case is what we really want. We're interested in the common case, which requires years of empirical observation. While it is certainly possible that we'll slowly be able to improve formal verification for the common case (as an industry user of formal methods, I certainly hope so and believe it will happen in a few decades), there is no current indication that this would ever be affordable. Currently, proof of correctness of anything larger than a few hundreds or a couple of thousands LOC is simply out of reach for the foreseeable future. So I'm not assuming anything, just stating the worst-case, and noting that there is no empirical indication that the common case is significantly better. > That's precisely why I'm not interested in mechanical verification anymore. Well, that's the only approach that has been shown to work in practice on real world software so far -- and they work very well (although, again, not quite in the way people who have not had experience with formal methods think). Deductive proofs (with Isabelle, PVS, Coq etc.) is used only to tie together results of automated methods, or fill in the holes where automated methods have failed. Doing it any other way is simply not economical. Even the most avid supporters of manual verification (who've actually tried it on nontrivial software) would agree. I don't think anyone believes that "ordinary" non-high-assurance real software (aside from certain very small core components) would be verified by deductive proof any time in the next few decades. The only people who believe otherwise are those who haven't actually tried formal methods on real-world software. > The difficulty lies elsewhere: in the extremely low probability that an unverified program will be correct. But software requirements aren't for 100% confidence in correctness, if only because you don't get anywhere near that with the hardware the software is running on. So the question is precisely how much more correct a software is with increasing verification effort. Like I said, there appears to be a pretty steep curve of diminishing returns. End-to-end verification is almost never affordable, but it is also almost never required. What the formal methods community is really interested in these days is how to reduce the cost of verification required to achieve current (and near-future) correctness requirements.