3 ms·

Disappointing to see such a long article and no mention of type theory, or any other work from the "correct by construction" school of formal methods. It's all

Disappointing to see such a long article and no mention of type theory, or any other work from the "correct by construction" school of formal methods. It's all normie model checking, TLA+ etc.

AnimalMuppet 9y ago
Type theory is much less than "correct by construction" formal methods. Type theory is great at preventing a whole class of bugs (an operation on a value for which that operation doesn't make sense). But it's inadequate for the larger problem, of whether the operation is the correct one. Formal methods can ensure that the code matches a formally written spec, for all the aspects of the code that are covered by the formal method. Note well: That's not all aspects of the code. And you have the little problem of (correctly) creating the formal spec. This move the problem up a layer, but the problem doesn't go away. Even given a formal spec, though, it's my impression that formal methods are s l o w. Does anyone have data on this?
- catnaroek 9y ago
  > And you have the little problem of (correctly) creating the formal spec. How on Earth did we end up putting people who can't write down precisely what they want in charge of programming machines that do exactly what you tell them to?
  - perl4ever 9y ago
    I was just told today that gathering requirements is not my job, it's the PM's. But they are swamped in administrative minutiae, and all too often the only person who knows how something worked has quit anyway. So in sum "no spec, no spec, you're the spec!"
- kmicklas 9y ago
  > But it's inadequate for the larger problem, of whether the operation is the correct one. Huh? Types (of the sufficiently advanced kind) are one way of specifying behavior in the same sense as TLA+ and other models. The difference is that type theory provides a coherent story for how to form entire systems like this in a composable manner. Traditional modeling/spec languages, not so much.
  - hwayne 9y ago
    What are some good examples of complex system properties you've seen verified with sufficiently advanced types?
    - kmicklas 9y ago
      Probably the poster children of verification: * http://compcert.inria.fr/ http://compcert.inria.fr/ * https://sel4.systems/ https://sel4.systems/

Disappointing to see such a long article and no mention of type theory, or any other work from the "correct by construction" school of formal methods. It's all normie model checking, TLA+ etc.

AnimalMuppet 9y ago

Type theory is much less than "correct by construction" formal methods. Type theory is great at preventing a whole class of bugs (an operation on a value for which that operation doesn't make sense). But it's inadequate for the larger problem, of whether the operation is the correct one. Formal methods can ensure that the code matches a formally written spec, for all the aspects of the code that are covered by the formal method. Note well: That's not all aspects of the code. And you have the little problem of (correctly) creating the formal spec. This move the problem up a layer, but the problem doesn't go away. Even given a formal spec, though, it's my impression that formal methods are s l o w. Does anyone have data on this?

catnaroek 9y ago
> And you have the little problem of (correctly) creating the formal spec. How on Earth did we end up putting people who can't write down precisely what they want in charge of programming machines that do exactly what you tell them to?
- perl4ever 9y ago
  I was just told today that gathering requirements is not my job, it's the PM's. But they are swamped in administrative minutiae, and all too often the only person who knows how something worked has quit anyway. So in sum "no spec, no spec, you're the spec!"
kmicklas 9y ago
> But it's inadequate for the larger problem, of whether the operation is the correct one. Huh? Types (of the sufficiently advanced kind) are one way of specifying behavior in the same sense as TLA+ and other models. The difference is that type theory provides a coherent story for how to form entire systems like this in a composable manner. Traditional modeling/spec languages, not so much.
- hwayne 9y ago
  What are some good examples of complex system properties you've seen verified with sufficiently advanced types?
  - kmicklas 9y ago
    Probably the poster children of verification: * http://compcert.inria.fr/ http://compcert.inria.fr/ * https://sel4.systems/ https://sel4.systems/