5 ms·

Several comments elaborate on the big gap between normal programming practice (e.g. structurally recursive algorithms) and the great difficulty of dependent typ

Several comments elaborate on the big gap between normal programming practice (e.g. structurally recursive algorithms) and the great difficulty of dependent typing those practices. Some of these comment on how dependent types are "just out of the lab". This brings into focus a question I've had for a long time: Why this gap, and especially in this direction? E.g. in aerodynamics we had Bernoulli's principle for a couple of hundred years before we could build airplanes, which depend on it. In formal language theory we had lambda calculus, Turing's universality results, etc. decades before we had Lisp and Fortran. We often see the difficulty of building a practice to exploit theory. So it seems very strange to me that we are able to write / plug together literally world-spanning software systems -- which do have bugs but fact work correctly nearly all the time. But we can't easily well-type even simple algorithms with extremely well understood properties. Why this huge gap, in this direction?

KirinDave 8y ago
I'd argue that there aren't many "simple" programs with "well-understood" properties in use in industry. Software is a bit different from architecture in that partial failures tend to work and can be refined around repeatedly (a partially failed building tends to rip itself apart, partial failures in software can linger for years and only cease when their dependencies fault out). People are just more amenable to altering their processes, products and lives around bad software. I think dependent typing reveals to us, to some extent, what a house of cards we truly have built for ourselves.
- jedharris 8y ago
  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

I'd argue that there aren't many "simple" programs with "well-understood" properties in use in industry. Software is a bit different from architecture in that partial failures tend to work and can be refined around repeatedly (a partially failed building tends to rip itself apart, partial failures in software can linger for years and only cease when their dependencies fault out). People are just more amenable to altering their processes, products and lives around bad software. I think dependent typing reveals to us, to some extent, what a house of cards we truly have built for ourselves.

jedharris 8y ago
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.