3 ms·

Another question is whether translation from TLA to, say Haskell or Scala is on the roadmap? That would be a killer feature but I've never heard this being some

Another question is whether translation from TLA to, say Haskell or Scala is on the roadmap? That would be a killer feature but I've never heard this being something that is planned for implementation.

carterschonwald 8y ago
I’ve actually found translation between tla plus and Haskell or agda pretty straight forward using what I call the coinductive approach (which could also be called purely functional OOP done right), I have some examples I shared on reddit two years ago https://www.reddit.com/r/haskell/comments/4aju8f/simple_example_of_emulating_copattern_matching_in/ https://www.reddit.com/r/haskell/comments/4aju8f/simple_exam...
virgilp 8y ago
It would be impossible. The whole point of TLA is to test & document the high-level design. You can only generate complete implementation for toy problems (and that is a feature)
- pron 8y ago
  I wouldn't say that's "the whole point." You can specify at any level you choose, even electronic circuits (in fact, TLA+ has been successfully used in the design of microprocessors). It's just that the most effective general-purpose use of formal methods, given our current technology, is in a high-level design (where high-level is relative to whatever your domain is), as formal methods are constrained by a certain amount of detail, and therefore it is best to use that budget on the actual tricky/subtle parts of the problem, rather than waste it on stuff that's fairly simple (translating the spec into code, which is simple but contains a lot of "uninteresting" detail).
  - virgilp 8y ago
    I would still say that, though. For complex/ non-"toy" systems, the required level of detail increases so much, that if you specify it all in something like TLA+, even ignoring the performance aspects, it probably becomes too hard to understand it all and you lose most of the advantage that TLA+ is supposed to give you. It's not just about the "formal verification" part - it's about the whole cycle of model -> verify -> learn/improve understanding -> improve model. And the fact that it was used to design microprocessors doesn't say that it can or should be used to specify all the details. I bet nobody ever attempted to do the layout from the TLA+ model; it's just like in software, TLA+ was used to design geo-distributed databases... but not to write any piece of the code; just to check that the general design is right.
    - pron 8y ago
      > it probably becomes too hard to understand it all and you lose most of the advantage that TLA+ is supposed to give you. Not necessarily. There are tools that compile C or Java to TLA+[1]. But, like all other code-level reasoning, when using them you are limited to very small programs. > It's not just about the "formal verification" part - it's about the whole cycle of model -> verify -> learn/improve understanding -> improve model. I agree, but again, that's because TLA+ is intended for industry use, not as a research tool, and as we simply don't have the technology to verify most real programs all the way down to code, TLA+ places an emphasis on the best ROI you can get from formal methods, in practice, given current technology. [1]: https://link.springer.com/chapter/10.1007%2F978-3-319-17581-2_14 https://link.springer.com/chapter/10.1007%2F978-3-319-17581-...

carterschonwald 8y ago

I’ve actually found translation between tla plus and Haskell or agda pretty straight forward using what I call the coinductive approach (which could also be called purely functional OOP done right), I have some examples I shared on reddit two years ago https://www.reddit.com/r/haskell/comments/4aju8f/simple_example_of_emulating_copattern_matching_in/ https://www.reddit.com/r/haskell/comments/4aju8f/simple_exam...

virgilp 8y ago

It would be impossible. The whole point of TLA is to test & document the high-level design. You can only generate complete implementation for toy problems (and that is a feature)

pron 8y ago
I wouldn't say that's "the whole point." You can specify at any level you choose, even electronic circuits (in fact, TLA+ has been successfully used in the design of microprocessors). It's just that the most effective general-purpose use of formal methods, given our current technology, is in a high-level design (where high-level is relative to whatever your domain is), as formal methods are constrained by a certain amount of detail, and therefore it is best to use that budget on the actual tricky/subtle parts of the problem, rather than waste it on stuff that's fairly simple (translating the spec into code, which is simple but contains a lot of "uninteresting" detail).
- virgilp 8y ago
  I would still say that, though. For complex/ non-"toy" systems, the required level of detail increases so much, that if you specify it all in something like TLA+, even ignoring the performance aspects, it probably becomes too hard to understand it all and you lose most of the advantage that TLA+ is supposed to give you. It's not just about the "formal verification" part - it's about the whole cycle of model -> verify -> learn/improve understanding -> improve model. And the fact that it was used to design microprocessors doesn't say that it can or should be used to specify all the details. I bet nobody ever attempted to do the layout from the TLA+ model; it's just like in software, TLA+ was used to design geo-distributed databases... but not to write any piece of the code; just to check that the general design is right.
  - pron 8y ago
    > it probably becomes too hard to understand it all and you lose most of the advantage that TLA+ is supposed to give you. Not necessarily. There are tools that compile C or Java to TLA+[1]. But, like all other code-level reasoning, when using them you are limited to very small programs. > It's not just about the "formal verification" part - it's about the whole cycle of model -> verify -> learn/improve understanding -> improve model. I agree, but again, that's because TLA+ is intended for industry use, not as a research tool, and as we simply don't have the technology to verify most real programs all the way down to code, TLA+ places an emphasis on the best ROI you can get from formal methods, in practice, given current technology. [1]: https://link.springer.com/chapter/10.1007%2F978-3-319-17581-2_14 https://link.springer.com/chapter/10.1007%2F978-3-319-17581-...