5 ms·

Several interesting points but maybe they show something different from what you intend. Network stacks, databases etc. that correctly handle trillions of inte

Several interesting points but maybe they show something different from what you intend. Network stacks, databases etc. that correctly handle trillions of interactions, some of them adversarial, have indeed been "refined around [their failures] repeatedly" and have gotten pretty robust along the way. On the other hand useful formal accounts of their behavior (distributed, highly parallel, loosely coupled, asynchronous) seem far, far way. It would be helpful to have an account of approximation to formal properties, especially if that can help us understand how repair and refactoring can lead to progressively better approximations. Perhaps the house of cards that is revealed is formal methods not software.

KirinDave 8y ago
> Network stacks, databases etc. that correctly handle trillions of interactions, But they have also incorrectly handled a similar order of magnitude of transactions! Routing failures and issues that people troubleshoot around, misconfigurations and bugs, and simple electromechanical glitches exist in the real world and they're not some kind of zebra, you can force them by pining a server. Our networking systems "mostly work" because they're persistent, and because (interestingly) the difference between a perfectly coordinated networking system and a purely chaotic networking system with random traffic is actually rather small compared to other domains. > On the other hand useful formal accounts of their behavior (distributed, highly parallel, loosely coupled, asynchronous) seem far, far way. Generally what makes a difference between a "robust" program and a brittle program that simply falls over is how much of its own failure it attempts to take into account. Even bad models of self-failure (pre-OTP erlang, for example) are better than no model at all. > Perhaps the house of cards that is revealed is formal methods not software. Given that almost no one applies formal methods and dependent typing is by no means a part of that discipline, I'm not sure it's fair to draw those comparisons in this conversation. Dependent Typing is not formal methods, nor is it verifcation. It's code that allows for automated reasoning. It's closer to the machinery of formal methods, like datalog or an SMT solver.
- jedharris 8y ago
  Again lots of interesting points. Only time for one response. You highlight networking but I also mentioned databases. Schematizing your comment "Our... systems "mostly work" because... the difference between a perfectly coordinated... system and a purely chaotic... system... is actually rather small". I think banks and customers would disagree rather violently regarding the (distributed, asynchronous) system that handles credit card transactions. And yet this system is certainly subject to a lot of attacks, not just random errors.
  - KirinDave 8y ago
    > I think banks and customers would disagree rather violently regarding the (distributed, asynchronous) system that handles credit card transactions. Do they? Most customers accept without question the idea that they have an "available" balance distinct from their "current" balance. It's also the case that when attacked the system typically fails and then the fungibility of currency combined with the massive power of insurance is used to pave over it.

KirinDave 8y ago

> Network stacks, databases etc. that correctly handle trillions of interactions, But they have also incorrectly handled a similar order of magnitude of transactions! Routing failures and issues that people troubleshoot around, misconfigurations and bugs, and simple electromechanical glitches exist in the real world and they're not some kind of zebra, you can force them by pining a server. Our networking systems "mostly work" because they're persistent, and because (interestingly) the difference between a perfectly coordinated networking system and a purely chaotic networking system with random traffic is actually rather small compared to other domains. > On the other hand useful formal accounts of their behavior (distributed, highly parallel, loosely coupled, asynchronous) seem far, far way. Generally what makes a difference between a "robust" program and a brittle program that simply falls over is how much of its own failure it attempts to take into account. Even bad models of self-failure (pre-OTP erlang, for example) are better than no model at all. > Perhaps the house of cards that is revealed is formal methods not software. Given that almost no one applies formal methods and dependent typing is by no means a part of that discipline, I'm not sure it's fair to draw those comparisons in this conversation. Dependent Typing is not formal methods, nor is it verifcation. It's code that allows for automated reasoning. It's closer to the machinery of formal methods, like datalog or an SMT solver.

jedharris 8y ago
Again lots of interesting points. Only time for one response. You highlight networking but I also mentioned databases. Schematizing your comment "Our... systems "mostly work" because... the difference between a perfectly coordinated... system and a purely chaotic... system... is actually rather small". I think banks and customers would disagree rather violently regarding the (distributed, asynchronous) system that handles credit card transactions. And yet this system is certainly subject to a lot of attacks, not just random errors.
- KirinDave 8y ago
  > I think banks and customers would disagree rather violently regarding the (distributed, asynchronous) system that handles credit card transactions. Do they? Most customers accept without question the idea that they have an "available" balance distinct from their "current" balance. It's also the case that when attacked the system typically fails and then the fungibility of currency combined with the massive power of insurance is used to pave over it.