5 ms·

Have you read Ghosts of Departed Proofs? I agree there haven’t been enough studies. Sufficiently advanced type systems do enable us to express specifications th

Have you read Ghosts of Departed Proofs? I agree there haven’t been enough studies. Sufficiently advanced type systems do enable us to express specifications that can check our implementation. It’s not on the level of model checkers or proof assistants but it is an awfully effective tool for constructing programs that are functionally correct with respect to their specification, faster.

pron 7y ago
Yes, I have, but the question here isn't whether types can be used to verify any correctness property, but whether, overall, there is some correlation between the type system and functional correctness, and there doesn't seem to be one. The question is why this is the case. Perhaps it is because types are not any more effective in their cost/benefit than other ways of increasing correctness. Papers like that are driven by what can be verified with a chosen approach, not by cost/benefit and comparison with other approaches. In other words, they show some property without assigning it a relative value. Pointing at such papers when discussing correctness relative to other languages is like telling people they'd be much better off working at company A rather than company B, because company A gives out free lunches. Even if company B doesn't, it might offer free dinner, and even if it doesn't the salary can be higher, and even if not, it's unclear how big of a difference A's lunch is. In other words, correctness is very complicated, and there is just no way to look at one property or another and make a conclusion. Indeed, there does not seem to be a big difference in practice.
- agentultra 7y ago
  In the absence of enough studies I find it difficult to draw any hard conclusions. I think type systems, such as Haskell’s, strike a good balance between formal and informal specifications such as unit tests or diagrams of boxes and arrows.
  - pron 7y ago
    > In the absence of enough studies I find it difficult to draw any hard conclusions. Me too, which is why I say that it does not seem to make a big positive or negative difference (big differences are easy to find; there haven't been enough studies about the correlation between eating lettuce and baldness so we cannot draw any hard conclusion about there being a correlation or not, and should continue assuming that it's likely not a big cause for baldness nor a definitive cure). > I think type systems, such as Haskell’s, strike a good balance between formal and informal specifications such as unit tests or diagrams of boxes and arrows. I agree. Haskell's type system is OK, and I think most other languages also strike a balance that is roughly equally good, albeit not necessarily through the type system, which is why Haskell doesn't appear to be doing much worse or much better at the bottom line. So I definitely see no good reason to suggest Haskell should lead to drastically lower correctness, and if someone said they cared about correctness and want to use Haskell, I wouldn't think it's an exceptionally bad choice. I think (simple) type systems have many good benefits (code organization, documentation, tooling, AOT-compilation performance), which is why I like them, but correctness just isn't one of them. And why should it be? Theory certainly does not suggest simple types should have a big impact on correctness. The strength of the Haskell type system is such that for most uses of it, for any well-typed Haskell program, there is a very small finite-state program that satisfies the same type (expressible as a very small program), yet clearly most of what the program does -- as well as its code -- lies well beyond its type-equivalent small FSM. So any argument that says that the type would still have a big impact of correctness despite the theory saying it shouldn't would also need to explain why other techniques, like tests without a type system, aren't at least as effective (cost/benefit-wise).
    - naasking 7y ago
      > I think (simple) type systems have many good benefits (code organization, documentation, tooling, AOT-compilation performance), which is why I like them, but correctness just isn't one of them Most of those impact correctness (amongst other benefits), otherwise we wouldn't care about them. None of the studies that have been carried out tested the long-term benefits of types, which is precisely where types would shine,so I cannot agree with your conclusions in this thread.

pron 7y ago

Yes, I have, but the question here isn't whether types can be used to verify any correctness property, but whether, overall, there is some correlation between the type system and functional correctness, and there doesn't seem to be one. The question is why this is the case. Perhaps it is because types are not any more effective in their cost/benefit than other ways of increasing correctness. Papers like that are driven by what can be verified with a chosen approach, not by cost/benefit and comparison with other approaches. In other words, they show some property without assigning it a relative value. Pointing at such papers when discussing correctness relative to other languages is like telling people they'd be much better off working at company A rather than company B, because company A gives out free lunches. Even if company B doesn't, it might offer free dinner, and even if it doesn't the salary can be higher, and even if not, it's unclear how big of a difference A's lunch is. In other words, correctness is very complicated, and there is just no way to look at one property or another and make a conclusion. Indeed, there does not seem to be a big difference in practice.

agentultra 7y ago
In the absence of enough studies I find it difficult to draw any hard conclusions. I think type systems, such as Haskell’s, strike a good balance between formal and informal specifications such as unit tests or diagrams of boxes and arrows.
- pron 7y ago
  > In the absence of enough studies I find it difficult to draw any hard conclusions. Me too, which is why I say that it does not seem to make a big positive or negative difference (big differences are easy to find; there haven't been enough studies about the correlation between eating lettuce and baldness so we cannot draw any hard conclusion about there being a correlation or not, and should continue assuming that it's likely not a big cause for baldness nor a definitive cure). > I think type systems, such as Haskell’s, strike a good balance between formal and informal specifications such as unit tests or diagrams of boxes and arrows. I agree. Haskell's type system is OK, and I think most other languages also strike a balance that is roughly equally good, albeit not necessarily through the type system, which is why Haskell doesn't appear to be doing much worse or much better at the bottom line. So I definitely see no good reason to suggest Haskell should lead to drastically lower correctness, and if someone said they cared about correctness and want to use Haskell, I wouldn't think it's an exceptionally bad choice. I think (simple) type systems have many good benefits (code organization, documentation, tooling, AOT-compilation performance), which is why I like them, but correctness just isn't one of them. And why should it be? Theory certainly does not suggest simple types should have a big impact on correctness. The strength of the Haskell type system is such that for most uses of it, for any well-typed Haskell program, there is a very small finite-state program that satisfies the same type (expressible as a very small program), yet clearly most of what the program does -- as well as its code -- lies well beyond its type-equivalent small FSM. So any argument that says that the type would still have a big impact of correctness despite the theory saying it shouldn't would also need to explain why other techniques, like tests without a type system, aren't at least as effective (cost/benefit-wise).
  - naasking 7y ago
    > I think (simple) type systems have many good benefits (code organization, documentation, tooling, AOT-compilation performance), which is why I like them, but correctness just isn't one of them Most of those impact correctness (amongst other benefits), otherwise we wouldn't care about them. None of the studies that have been carried out tested the long-term benefits of types, which is precisely where types would shine,so I cannot agree with your conclusions in this thread.