6 ms·

> We don't have such (real) languages yet We do. Because Haskell and ML are ultimately just fancy term rewriting systems, you can do equational reasoning on th

> We don't have such (real) languages yet We do. Because Haskell and ML are ultimately just fancy term rewriting systems, you can do equational reasoning on their terms by hand just fine. It's even easy enough for non-[computer scientists/mathematicians] (such as yours truly) to do it casually!

pron 11y ago
Like I said above, Haskell/ML's type systems don't even come close to verifying most interesting program properties. They can't even verify a monad, let alone the simplest sorting (or selection) algorithm. All those software verification tools most certainly can, and even much more interesting properties/algorithms than that. Esterel can't verify a sorting algorithm (as it can't even express it), but it can verify most properties that interest developers of safety-critical control systems, including timing and memory use.
- catnaroek 11y ago
  «can't verify a monad» (probably you meant «that the monad laws hold») More often than not, either the monad laws are easy to verify by hand (exceptions, state, nondeterminism, etc.) or the verification can be borrowed from nLab. It's a nonproblem. As I said in another comment, there's no general technique or tool for proving arbitrary theorems, and we have to live with that. Sometimes I use a type checker, other times I grab a pen and a piece of paper and carry out the proof by hand. Quantifier-free equational reasoning makes the latter super easy.
  - pron 11y ago
    > It's a nonproblem. And that's exactly what can be said about the difference between Haskell's and Java's type systems. It hasn't been shown that the additional provable properties -- that are not too powerful -- do in fact result in cheaper development. I.e. you haven't shown that Haskell's rich type system solves a real problem. That requires empirical evidence. > Sometimes I use a type checker, other times I grab a pen and a piece of paper and carry out the proof by hand. Quantifier-free equational reasoning makes the latter super easy. But you said "perform your proofs in the same term language in which your program is written". If the actual interesting verification is done by other tools why is your approach better than Amazon's (write in Java, verify in TLA+)?
    - tome 11y ago
      > result in cheaper development. I.e. you haven't shown that Haskell's rich type system solves a real problem I think there's too little agreement in this thread about what "cheaper" and "real problem" mean. I certainly find that Haskell "more cheaply" (i.e. with less mental burden) allows me, as an individual, to write programs more easily. Whether that observation scales to everyone is a very hard question to answer. > But you said "perform your proofs in the same term language in which your program is written". If the actual interesting verification is done by other tools why is your approach better than Amazon's (write in Java, verify in TLA+)? On the face of it, proving by manipulating Haskell expressions certainly compares favourably to proving with TLA+ and then translating into Haskell (or other language). There may, on the other hand, be additional tooling advantages around TLA+.
      - catnaroek 11y ago
        > I think there's too little agreement in this thread about what "cheaper" and "real problem" mean. I certainly find that Haskell "more cheaply" (i.e. with less mental burden) allows me, as an individual, to write programs more easily. Whether that observation scales to everyone is a very hard question to answer. I think he was talking in monetary terms. And this is a useful point of view. While Haskell's beauty makes writing Haskell its own reward for some (at least me), from a practical point of view, we ought to ask ourselves «Can we actually turn Haskell's elegance into a business competitive advantage?» And, then, there's a reason why I don't run a business...
        tome 11y ago
        > I think he was talking in monetary terms. I think so too, but even then there are a lot of unanswered questions. > from a practical point of view, we ought to ask ourselves «Can we actually turn Haskell's elegance into a business competitive advantage?» And, then, there's a reason why I don't run a business... I do run a business and do believe that Haskell gives me a competitive advantage, of a sort. The interesting question is not whether this is true, but in what precise sense it is true.

pron 11y ago

Like I said above, Haskell/ML's type systems don't even come close to verifying most interesting program properties. They can't even verify a monad, let alone the simplest sorting (or selection) algorithm. All those software verification tools most certainly can, and even much more interesting properties/algorithms than that. Esterel can't verify a sorting algorithm (as it can't even express it), but it can verify most properties that interest developers of safety-critical control systems, including timing and memory use.

catnaroek 11y ago
«can't verify a monad» (probably you meant «that the monad laws hold») More often than not, either the monad laws are easy to verify by hand (exceptions, state, nondeterminism, etc.) or the verification can be borrowed from nLab. It's a nonproblem. As I said in another comment, there's no general technique or tool for proving arbitrary theorems, and we have to live with that. Sometimes I use a type checker, other times I grab a pen and a piece of paper and carry out the proof by hand. Quantifier-free equational reasoning makes the latter super easy.
- pron 11y ago
  > It's a nonproblem. And that's exactly what can be said about the difference between Haskell's and Java's type systems. It hasn't been shown that the additional provable properties -- that are not too powerful -- do in fact result in cheaper development. I.e. you haven't shown that Haskell's rich type system solves a real problem. That requires empirical evidence. > Sometimes I use a type checker, other times I grab a pen and a piece of paper and carry out the proof by hand. Quantifier-free equational reasoning makes the latter super easy. But you said "perform your proofs in the same term language in which your program is written". If the actual interesting verification is done by other tools why is your approach better than Amazon's (write in Java, verify in TLA+)?
  - tome 11y ago
    > result in cheaper development. I.e. you haven't shown that Haskell's rich type system solves a real problem I think there's too little agreement in this thread about what "cheaper" and "real problem" mean. I certainly find that Haskell "more cheaply" (i.e. with less mental burden) allows me, as an individual, to write programs more easily. Whether that observation scales to everyone is a very hard question to answer. > But you said "perform your proofs in the same term language in which your program is written". If the actual interesting verification is done by other tools why is your approach better than Amazon's (write in Java, verify in TLA+)? On the face of it, proving by manipulating Haskell expressions certainly compares favourably to proving with TLA+ and then translating into Haskell (or other language). There may, on the other hand, be additional tooling advantages around TLA+.
    - catnaroek 11y ago
      > I think there's too little agreement in this thread about what "cheaper" and "real problem" mean. I certainly find that Haskell "more cheaply" (i.e. with less mental burden) allows me, as an individual, to write programs more easily. Whether that observation scales to everyone is a very hard question to answer. I think he was talking in monetary terms. And this is a useful point of view. While Haskell's beauty makes writing Haskell its own reward for some (at least me), from a practical point of view, we ought to ask ourselves «Can we actually turn Haskell's elegance into a business competitive advantage?» And, then, there's a reason why I don't run a business...
      - tome 11y ago
        > I think he was talking in monetary terms. I think so too, but even then there are a lot of unanswered questions. > from a practical point of view, we ought to ask ourselves «Can we actually turn Haskell's elegance into a business competitive advantage?» And, then, there's a reason why I don't run a business... I do run a business and do believe that Haskell gives me a competitive advantage, of a sort. The interesting question is not whether this is true, but in what precise sense it is true.