4 ms·

«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

«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.
      - catnaroek 11y ago
        > I do run a business and do believe that Haskell gives me a competitive advantage, of a sort. Wow, nice! :-)
  - pron 11y ago
    > proving by manipulating Haskell expressions certainly compares favourably to proving with TLA+ and then translating into Haskell Yes, but you don't prove the same properties with Haskell as with TLA+ (in fact, I think that there is little overlap if any in practice). Most properties proven (well, maybe not proven but satisfactorily verified) with TLA+ (or any other sophisticated verification tool) just can't be proven in Haskell. And, again, I even prefer TLA+ to JPF (which is the tool I've had most experience with) which verifies Java bytecode directly because so far I find it more effective to verify only the core components of the algorithm. Verifying the details is usually a waste of effort (they both make the verification harder -- either harder to prove if you're doing a formal proof, or much longer to run in a model checker -- and they are easy to verify by other, informal means).
- catnaroek 11y ago
  > And that's exactly what can be said about the difference between Haskell's and Java's type systems. This is a little bit disingenuous, for reasons exposed below. > 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. No disagreement here. I don't recall ever making any statements myself to the tone of «Haskell makes writing correct programs cheaper». But if someone else told you that, you're right - it requires empirical evidence. > But you said "perform your proofs in the same term language in which your program is written". And it is. Equational reasoning about Haskell programs is just using Haskell's existing reduction relation, extended with additional assumed identifications that can be used as reductions in either direction (given `a = b`, replacing either `a` for `b` or vice versa, though more often than not, only one direction is needed). Only at the last step do we need a check that two Haskell terms are syntactically equal, which, as you say, is not doable in Haskell itself (since judgmental term equality isn't first-class), although it is trivial to do by visual inspection. The fact remains that the bulk of the work of verifying non-IO Haskell code is really just evaluating Haskell code. > If the actual interesting verification is done by other tools why is your approach better than Amazon's (write in Java, verify in TLA+)? I can't comment on what's best for Amazon's needs, since I've never worked there. And, obviously, there's a lot more software engineering talent working for Amazon than sitting in front of my keyboard. That being said, I think the amount of effort required to evaluate Haskell[0] by hand is significantly less than the amount of effort required to translate back and forth between Java and TLA+. And, for my needs (mainly implementing compilers and libraries of data structures and algorithms), Haskell is a significantly better language than Java (or Lisp, Python, C++, what have you). Precisely because I can reason about Haskell programs by just evaluating Haskell[0] by hand, whereas doing the same in Java would require me to constantly translate back and forth between Java and an external logic. --- [0] Plus propositional equalities.
  - pron 11y ago
    > Only at the last step do we need a check that two Haskell terms are syntactically equal I'm sorry, but that's just not true, or, more precisely, it's not necessarily doable in practice. For one, there's bounded recursion which may not be so easy to substitute, and that recursion interacts with equality to yield much richer properties. For example, if you pick a recursive QuickSort implementation (just picked sorting because that's a classical verification example) and wanted to verify it in Haskell, you'll need to prove much more than equality at each recursive step (or unwind the entire computation and then prove equality, but that's not a very convenient proof). Second, most interesting algorithms make use of time and state, so you'd need to prove past the semantics of the effect monad (STM, threads, whatever), and that also requires much more than simple equality (TLA+ and Esterel use temoporal logic, which is awesome, and I think Coq et al. use dependent types to encode modal logic, but I don't know how it's done or whether that's the approach). Haskell's logic is only marginally helpful in these scenarios and I don't know if translating from TLA+ to Java is harder or more error-prone than translating to Haskell, and even if it were, the difference (again, conjecture and gut feeling) seems to be marginal to offset the many other benefits of using Java. There are some interesting uses of Haskell's logic, such as session types (also possible in Java, BTW), but they are too underpowered to prove any distributed algorithm of interest (AFAICT, they are exactly as powerful as regular expressions). What bothers me most about Haskell's approach -- and correct me if I'm wrong -- is that the strength of the type system is pretty much defined to be "anything that's inferrable by an extended HM algorithm", which means that the strength is arbitrarily chosen to match a "convenience point" arbitrarily defined to be "full program inference", rather than an analysis of what strength is needed, and then tweaking it to trade off some strength for convenience. So it is the features of a certain algorithm which determines the language's semantics rather than an analysis of what's helpful. Good examples of the latter approach would be Java, Erlang and Clojure. (BTW, a good explanation of Java's design decision is in the first 17 minutes or so of this talk: https://www.youtube.com/watch?v=Dq2WQuWVrgQ https://www.youtube.com/watch?v=Dq2WQuWVrgQ) That is somehow (if you squint) similar to Prolog, whose utility was determined by the quality of it search algorithms. Such approach makes for great research, but its industrial applicability is very brittle. > Haskell is a significantly better language than Java ... Precisely because I can reason about Haskell programs by just evaluating Haskell by hand, whereas doing the same in Java would require me to constantly translate back and forth between Java and an external logic. Even if I were to accept that premise, that only shows Haskell is better in some aspects (which I gladly acknowledge; Haskell is awesome![1]). A programming language is much more than that. In fact, I believe extra-linguistic features of the runtime -- e.g. GC, threading, performance, monitorability, hackability, profilability -- are a much bigger contributors to productivity (and cost) than syntax-level abstractions. But again, I have no proof, but some (strong) evidence (namely, the incredible productivity gain when the industry switched from C/C++ to Java -- which are intentionally syntactically similar but with drastic extra-linguistic changes -- and the difficulty achieving similar gains by other JVM languages (different syntax, same-or-similar extra-linguistic features). EDIT: Also, you kind of describe reduction as "just" substitution, but if Mr. Church has taught us anything it is that "just substitution" is computation, and is as powerful (well, not quite, but in some respects) as a Turing machine. So there's no reason to assume that "just substituting" is any easier for a human than simulating state, be it in the mind, on a piece of paper or in a debugger (or, better yet, one of Java's awesome time-travelling debuggers). I tend to think (without proof) that the human mind is actually better suited to state simulation than to substitution (we simulate stuff all the time; lambda substitution is a very mathematical concept). To make this more concrete, recursion is limited assignment, and recursion combined with a continuation (or, in Haskell, a continuation monad) is imperative assignment (imperative state can be fully implemented in a pure language with continuations and recursion). So substituting across the cont monads is directly more complicated (computationally -- it requires lots of reductions) than state simulation of the very same computation. [1]: But, forgive me, so is Java.

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.
    - catnaroek 11y ago
      > I do run a business and do believe that Haskell gives me a competitive advantage, of a sort. Wow, nice! :-)
- pron 11y ago
  > proving by manipulating Haskell expressions certainly compares favourably to proving with TLA+ and then translating into Haskell Yes, but you don't prove the same properties with Haskell as with TLA+ (in fact, I think that there is little overlap if any in practice). Most properties proven (well, maybe not proven but satisfactorily verified) with TLA+ (or any other sophisticated verification tool) just can't be proven in Haskell. And, again, I even prefer TLA+ to JPF (which is the tool I've had most experience with) which verifies Java bytecode directly because so far I find it more effective to verify only the core components of the algorithm. Verifying the details is usually a waste of effort (they both make the verification harder -- either harder to prove if you're doing a formal proof, or much longer to run in a model checker -- and they are easy to verify by other, informal means).
catnaroek 11y ago
> And that's exactly what can be said about the difference between Haskell's and Java's type systems. This is a little bit disingenuous, for reasons exposed below. > 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. No disagreement here. I don't recall ever making any statements myself to the tone of «Haskell makes writing correct programs cheaper». But if someone else told you that, you're right - it requires empirical evidence. > But you said "perform your proofs in the same term language in which your program is written". And it is. Equational reasoning about Haskell programs is just using Haskell's existing reduction relation, extended with additional assumed identifications that can be used as reductions in either direction (given `a = b`, replacing either `a` for `b` or vice versa, though more often than not, only one direction is needed). Only at the last step do we need a check that two Haskell terms are syntactically equal, which, as you say, is not doable in Haskell itself (since judgmental term equality isn't first-class), although it is trivial to do by visual inspection. The fact remains that the bulk of the work of verifying non-IO Haskell code is really just evaluating Haskell code. > If the actual interesting verification is done by other tools why is your approach better than Amazon's (write in Java, verify in TLA+)? I can't comment on what's best for Amazon's needs, since I've never worked there. And, obviously, there's a lot more software engineering talent working for Amazon than sitting in front of my keyboard. That being said, I think the amount of effort required to evaluate Haskell[0] by hand is significantly less than the amount of effort required to translate back and forth between Java and TLA+. And, for my needs (mainly implementing compilers and libraries of data structures and algorithms), Haskell is a significantly better language than Java (or Lisp, Python, C++, what have you). Precisely because I can reason about Haskell programs by just evaluating Haskell[0] by hand, whereas doing the same in Java would require me to constantly translate back and forth between Java and an external logic. --- [0] Plus propositional equalities.
- pron 11y ago
  > Only at the last step do we need a check that two Haskell terms are syntactically equal I'm sorry, but that's just not true, or, more precisely, it's not necessarily doable in practice. For one, there's bounded recursion which may not be so easy to substitute, and that recursion interacts with equality to yield much richer properties. For example, if you pick a recursive QuickSort implementation (just picked sorting because that's a classical verification example) and wanted to verify it in Haskell, you'll need to prove much more than equality at each recursive step (or unwind the entire computation and then prove equality, but that's not a very convenient proof). Second, most interesting algorithms make use of time and state, so you'd need to prove past the semantics of the effect monad (STM, threads, whatever), and that also requires much more than simple equality (TLA+ and Esterel use temoporal logic, which is awesome, and I think Coq et al. use dependent types to encode modal logic, but I don't know how it's done or whether that's the approach). Haskell's logic is only marginally helpful in these scenarios and I don't know if translating from TLA+ to Java is harder or more error-prone than translating to Haskell, and even if it were, the difference (again, conjecture and gut feeling) seems to be marginal to offset the many other benefits of using Java. There are some interesting uses of Haskell's logic, such as session types (also possible in Java, BTW), but they are too underpowered to prove any distributed algorithm of interest (AFAICT, they are exactly as powerful as regular expressions). What bothers me most about Haskell's approach -- and correct me if I'm wrong -- is that the strength of the type system is pretty much defined to be "anything that's inferrable by an extended HM algorithm", which means that the strength is arbitrarily chosen to match a "convenience point" arbitrarily defined to be "full program inference", rather than an analysis of what strength is needed, and then tweaking it to trade off some strength for convenience. So it is the features of a certain algorithm which determines the language's semantics rather than an analysis of what's helpful. Good examples of the latter approach would be Java, Erlang and Clojure. (BTW, a good explanation of Java's design decision is in the first 17 minutes or so of this talk: https://www.youtube.com/watch?v=Dq2WQuWVrgQ https://www.youtube.com/watch?v=Dq2WQuWVrgQ) That is somehow (if you squint) similar to Prolog, whose utility was determined by the quality of it search algorithms. Such approach makes for great research, but its industrial applicability is very brittle. > Haskell is a significantly better language than Java ... Precisely because I can reason about Haskell programs by just evaluating Haskell by hand, whereas doing the same in Java would require me to constantly translate back and forth between Java and an external logic. Even if I were to accept that premise, that only shows Haskell is better in some aspects (which I gladly acknowledge; Haskell is awesome![1]). A programming language is much more than that. In fact, I believe extra-linguistic features of the runtime -- e.g. GC, threading, performance, monitorability, hackability, profilability -- are a much bigger contributors to productivity (and cost) than syntax-level abstractions. But again, I have no proof, but some (strong) evidence (namely, the incredible productivity gain when the industry switched from C/C++ to Java -- which are intentionally syntactically similar but with drastic extra-linguistic changes -- and the difficulty achieving similar gains by other JVM languages (different syntax, same-or-similar extra-linguistic features). EDIT: Also, you kind of describe reduction as "just" substitution, but if Mr. Church has taught us anything it is that "just substitution" is computation, and is as powerful (well, not quite, but in some respects) as a Turing machine. So there's no reason to assume that "just substituting" is any easier for a human than simulating state, be it in the mind, on a piece of paper or in a debugger (or, better yet, one of Java's awesome time-travelling debuggers). I tend to think (without proof) that the human mind is actually better suited to state simulation than to substitution (we simulate stuff all the time; lambda substitution is a very mathematical concept). To make this more concrete, recursion is limited assignment, and recursion combined with a continuation (or, in Haskell, a continuation monad) is imperative assignment (imperative state can be fully implemented in a pure language with continuations and recursion). So substituting across the cont monads is directly more complicated (computationally -- it requires lots of reductions) than state simulation of the very same computation. [1]: But, forgive me, so is Java.