4 ms·

> Modularity doesn't mean compartmentalization, or isolation, of failure, which is impossible in general It's not impossible. There are two ways to do it: (0)

> Modularity doesn't mean compartmentalization, or isolation, of failure, which is impossible in general It's not impossible. There are two ways to do it: (0) Static: Prevent the deployment of incorrectly constructed modules. Obviously impossible in an evolutionary setting (life). (1) Dynamic: Require every module to check its own inputs, internal state and output. Admittedly, this is at odds with performance, which arguably matters most in a competitive setting (life). In general, I wouldn't borrow inspiration from biology. Life forms are too busy trying to survive to bother being perfect. But programmers have a moral obligation to be Intelligent Designers.

pron 10y ago
Oh, I'm not suggesting we borrow inspiration from biology at all, just pointing out that desired programming qualities are not features of a language but of programmer-language interaction, that's all (as is evident by those qualities appearing when a different kind of programmer -- natural selection -- uses a programming language which is unlikely to produce the same qualities for human programmers; conversely those qualities would not be replicated if natural selection were forced to use ML). 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[1]. 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. Checking the correctness of your input dynamically is also impossible in general because to know whether any arbitrary output of a black box is correct, the entire functionality of that black box must be replicated. In practice, there are solutions of both kinds that are as effective as the effort required to produce them, which invariably means some compromise must be made. [1]: See my post on computational complexity results of software verification: http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...
- catnaroek 10y ago
  > 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

Oh, I'm not suggesting we borrow inspiration from biology at all, just pointing out that desired programming qualities are not features of a language but of programmer-language interaction, that's all (as is evident by those qualities appearing when a different kind of programmer -- natural selection -- uses a programming language which is unlikely to produce the same qualities for human programmers; conversely those qualities would not be replicated if natural selection were forced to use ML). 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[1]. 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. Checking the correctness of your input dynamically is also impossible in general because to know whether any arbitrary output of a black box is correct, the entire functionality of that black box must be replicated. In practice, there are solutions of both kinds that are as effective as the effort required to produce them, which invariably means some compromise must be made. [1]: See my post on computational complexity results of software verification: http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...

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