5 ms·

> 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 thre

by 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).
- dllthomas 11y ago
  I've only dipped very shallowly into TLA+ and haven't had time to investigate, but I have been wondering if we can leverage Haskell's type system to make sure we're matching the abstractions we've assumed for TLA+ at a low cognitive overhead.

by tome 11y ago

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).

dllthomas 11y ago
I've only dipped very shallowly into TLA+ and haven't had time to investigate, but I have been wondering if we can leverage Haskell's type system to make sure we're matching the abstractions we've assumed for TLA+ at a low cognitive overhead.