3 ms·

Most of the complexity in today's “real world” software is accidental (i.e., a consequence of past bad decisions), not demanded by the problem domain, so the ar

Most of the complexity in today's “real world” software is accidental (i.e., a consequence of past bad decisions), not demanded by the problem domain, so the argument that “we can't handle real-world software” doesn't convince me. I'd rather live in a world where every program in a high-level language is no longer than, say, 5KLOC, but those 5KLOC are perfectly well understood by their authors and anyone else interested. As for the kinds of formal methods that you use: Mechanical verification no longer convinces me. It turns out that I don't just want to know whether a program is correct. I also want to know why it is correct, which parts of the program are closely related to which parts of the specification, how easily the program can be modified to satisfy a slightly different specification, etc., and these questions aren't easily answered by mechanical verification tools. (“Tweak the system's definition, re-run the tool” is for obvious reasons not satisfactory.) Considering that human understanding of the very systems we create should be the ultimate goal, I'd say that we shouldn't consider a system “proven correct” unless the proof can be communicated to a human. This means the proof itself should be short enough. If the proof requires running program to exhaustively verify a long list of cases (e.g., as done in the proof of the Four Color Theorem), at the very least the program itself should be short enough.

pron 10y ago
> Most of the complexity in today's “real world” software is accidental (i.e., a consequence of past bad decisions), not demanded by the problem domain I used to think that 20 years ago when I was a young programmer. But then I've seen the requirements for an air-traffic control system. 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. The world is very complicated and therefore so is software. > I'd rather live in a world where every program in a high-level language is no longer than, say, 5KLOC, but those 5KLOC are perfectly well understood by their authors and anyone else interested. Well, at the very least, that would be a world without computerized air-traffic control systems (I keep mentioning that example because that's something I worked on for some years). But the reality is that air-traffic control systems work, and thanks to them we can have many more airplanes in the air at any given time, and we very rarely get collisions. Also, we don't know how to prove most real-world 5KLOC programs yet. The largest program ever completely verified was probably seL4, and that was about 10KLOC of C; hardly a high-level language by today's standard. But let's say it's comparable to a 5K program. Now, seL4 took about 20 man years to write by a team of expert academics. I know someone on that team and they're confident they can do that a lot faster now. He says he'd figure about 5 man years (optimistically). That's 1 man year for 1000 LOC, by an optimistic estimate. But that's not all. 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). > Considering that human understanding of the very systems we create should be the ultimate goal, I'd say that we shouldn't consider a system “proven correct” unless the proof can be communicated to a human. I totally understand your wish that things were so, 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). I don't think you realize how small is the set of software that can be written in this way. But also, there's really no need. Why work so hard for simple software when we can get to similar failure levels as hardware with formal methods that are weaker than proof? Software doesn't live in a vacuum, and there's no point writing software for an airplane that's infinitely reliable if there's a real (albeit small) chance the wings might fall off.
- catnaroek 10y ago
  > 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

> Most of the complexity in today's “real world” software is accidental (i.e., a consequence of past bad decisions), not demanded by the problem domain I used to think that 20 years ago when I was a young programmer. But then I've seen the requirements for an air-traffic control system. 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. The world is very complicated and therefore so is software. > I'd rather live in a world where every program in a high-level language is no longer than, say, 5KLOC, but those 5KLOC are perfectly well understood by their authors and anyone else interested. Well, at the very least, that would be a world without computerized air-traffic control systems (I keep mentioning that example because that's something I worked on for some years). But the reality is that air-traffic control systems work, and thanks to them we can have many more airplanes in the air at any given time, and we very rarely get collisions. Also, we don't know how to prove most real-world 5KLOC programs yet. The largest program ever completely verified was probably seL4, and that was about 10KLOC of C; hardly a high-level language by today's standard. But let's say it's comparable to a 5K program. Now, seL4 took about 20 man years to write by a team of expert academics. I know someone on that team and they're confident they can do that a lot faster now. He says he'd figure about 5 man years (optimistically). That's 1 man year for 1000 LOC, by an optimistic estimate. But that's not all. 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). > Considering that human understanding of the very systems we create should be the ultimate goal, I'd say that we shouldn't consider a system “proven correct” unless the proof can be communicated to a human. I totally understand your wish that things were so, 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). I don't think you realize how small is the set of software that can be written in this way. But also, there's really no need. Why work so hard for simple software when we can get to similar failure levels as hardware with formal methods that are weaker than proof? Software doesn't live in a vacuum, and there's no point writing software for an airplane that's infinitely reliable if there's a real (albeit small) chance the wings might fall off.

catnaroek 10y ago
> 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.