3 ms·

> As to the question of failure isolation, your solutions do not work in general. Proving that a component is correct is intractable for all computational model

> As to the question of failure isolation, your solutions do not work in general. Proving that a component is correct is intractable for all computational models (even finite state machines) in general. That's because, in general, any random system you can come up with is crap. Even if evolution was good enough for Nature, we need Intelligent Design. (Or maybe not for you. Maybe you're happy with crap programs that only “work” in a statistical sense. I'm not.) > When it's done in practice, it is done at great effort, only on very small codebases, and even then at great cost both in effort and in design limitations. Where you see a limitation, I see a source of relief from not having to explore a design space that mostly consists of crap I wouldn't want to use, let alone maintain.

pron 10y ago
I have actually used formal methods on large, complex, real-word systems in my day job. This is how I know that even when using formal methods you must compromise. I find that the only people who think you can "just" prove programs correct are those who have never tried to do it for anything but a toy program. For example, Xavier Leroy, one of the worlds experts on deductive verification believes that the approach is feasible only for programs of a few hundred to a few thousands lines, and even then at a very high cost. Formal methods do work, and work very well, but not at all in the way people who have never used them on real-world systems think. Formal methods are on a spectrum of cost/benefit with an exponential curve of diminishing returns. For example, to go from, say, 98% confidence to 99.5% you need to expend about the same effort as going from 80% to 95%. Forget arbitrary or "random" software. While there have been teams who have worked months or years on deductively proving some program correct, no team has ever been able to prove the correctness of even a mid-sized application. You can set your standards as high as you like, but we cannot at the moment figure out how to completely prove the correctness of real-world software of any significant size even in principle.
- catnaroek 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, 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.
    - 10y ago

pron 10y ago

I have actually used formal methods on large, complex, real-word systems in my day job. This is how I know that even when using formal methods you must compromise. I find that the only people who think you can "just" prove programs correct are those who have never tried to do it for anything but a toy program. For example, Xavier Leroy, one of the worlds experts on deductive verification believes that the approach is feasible only for programs of a few hundred to a few thousands lines, and even then at a very high cost. Formal methods do work, and work very well, but not at all in the way people who have never used them on real-world systems think. Formal methods are on a spectrum of cost/benefit with an exponential curve of diminishing returns. For example, to go from, say, 98% confidence to 99.5% you need to expend about the same effort as going from 80% to 95%. Forget arbitrary or "random" software. While there have been teams who have worked months or years on deductively proving some program correct, no team has ever been able to prove the correctness of even a mid-sized application. You can set your standards as high as you like, but we cannot at the moment figure out how to completely prove the correctness of real-world software of any significant size even in principle.

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