4 ms·

After reading this post on HN about TLA+ a couple of days back, I started learning it: https://news.ycombinator.com/item?id=19661329 https://news.ycombinator.co

After reading this post on HN about TLA+ a couple of days back, I started learning it: https://news.ycombinator.com/item?id=19661329 https://news.ycombinator.com/item?id=19661329 And now I see this, and I'm already having second thoughts. Prima facie, what I like about DSLabs is it's not so steep learning curve as it's written in a mainstream OOP language. Can anyone who has worked on both TLA+ and DSLabs share thoughts?

nprescott 7y ago
While I haven't used DSLabs, I did suffer a similar bit of indecision recently trying to decide between Alloy[0] and TLA+[1]. In the end I don't think there is a correct answer, and there are probably more similarities than differences between any two specification languages. In my case I read both Software Abstractions and Specifying Systems (part 1 at least). Each took about a week; which is probably less time than I spent trying to decide between them. I happen to agree with the argument made by proponents of both TLA+ and Alloy that model checking and specification is better accomplished when detached from an implementation language, but I think you would benefit most from simply starting with one of them (DSLabs or TLA+) and decide later if you'd like to learn the other. [0]: http://alloytools.org/ http://alloytools.org/ [1]: https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html
- RBerenguel 7y ago
  I started learning TLA+ in October (or so), and after getting reasonably acceptable (as in, can write PlusCal without many issues, and can write and read basic plain TLA+) I'm starting to learn Alloy now. It offers a different approach that seems to suit different domains (say, less "temporal" focus)
agentultra 7y ago
I don't know about DSLabs' model checker but the advantage you get from TLA+ is that it's plain, simple maths. It can be used for specifying systems at many levels of abstraction that a programming language cannot. I'd be curious about how expressive DSLabs' language is, being based on Java -- can it express temporal properties as well as safety properties? As well the TLA+ toolbox has other tools in addition to the model checker: a pretty printer, and a proof system as well.
hwayne 7y ago
Speaking as a person who teaches both TLA+ and Alloy, I have a sneaking suspicion that the best way to learn the idea of model checking is _none of the three_. I haven't seriously sat down and deep dived yet, but I'm really liking what I've seen of Runway: https://runway.systems/ https://runway.systems/. It's advantages over all three are 1. A repl 2. A repl 3. You can try it online 4. Oh my god, there's a repl The core hasn't been updated in three years, so I'm not as ludicrously-overhyped on applying it to real systems, but to build your model thinking? I really like what I've seen so far.

nprescott 7y ago

While I haven't used DSLabs, I did suffer a similar bit of indecision recently trying to decide between Alloy[0] and TLA+[1]. In the end I don't think there is a correct answer, and there are probably more similarities than differences between any two specification languages. In my case I read both Software Abstractions and Specifying Systems (part 1 at least). Each took about a week; which is probably less time than I spent trying to decide between them. I happen to agree with the argument made by proponents of both TLA+ and Alloy that model checking and specification is better accomplished when detached from an implementation language, but I think you would benefit most from simply starting with one of them (DSLabs or TLA+) and decide later if you'd like to learn the other. [0]: http://alloytools.org/ http://alloytools.org/ [1]: https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html

RBerenguel 7y ago
I started learning TLA+ in October (or so), and after getting reasonably acceptable (as in, can write PlusCal without many issues, and can write and read basic plain TLA+) I'm starting to learn Alloy now. It offers a different approach that seems to suit different domains (say, less "temporal" focus)

agentultra 7y ago

I don't know about DSLabs' model checker but the advantage you get from TLA+ is that it's plain, simple maths. It can be used for specifying systems at many levels of abstraction that a programming language cannot. I'd be curious about how expressive DSLabs' language is, being based on Java -- can it express temporal properties as well as safety properties? As well the TLA+ toolbox has other tools in addition to the model checker: a pretty printer, and a proof system as well.

hwayne 7y ago

Speaking as a person who teaches both TLA+ and Alloy, I have a sneaking suspicion that the best way to learn the idea of model checking is _none of the three_. I haven't seriously sat down and deep dived yet, but I'm really liking what I've seen of Runway: https://runway.systems/ https://runway.systems/. It's advantages over all three are 1. A repl 2. A repl 3. You can try it online 4. Oh my god, there's a repl The core hasn't been updated in three years, so I'm not as ludicrously-overhyped on applying it to real systems, but to build your model thinking? I really like what I've seen so far.