I've considered using the command-line when I started using TLA+, but the manual discouraged it and I use it only occasionally so I didn't want to invest too much time on it.<p>I'd love to see a TLA+ package for vscode [1]. It seems there is more and more TLA+ adoption, it is surprising there aren't better environments to use it. The TLA Toolbox is awful (well, to be fair to the people that developed it, it does the job and maybe it's ok for some category of users).<p>EDIT: [1] there's one actually, <a href="https://github.com/TeamTilapia/vscode-tilapia" rel="nofollow">https://github.com/TeamTilapia/vscode-tilapia</a>
I am glad to see that I am not the only person who hates the TLA Toolbox. TLA+ is brilliant, but I always feel like an outsider using Vim to edit my specs.
The TLA+ Video Course by Leslie Lamport: <a href="https://news.ycombinator.com/item?id=16956778" rel="nofollow">https://news.ycombinator.com/item?id=16956778</a>
For those who care to provide constructive criticism, the TLA+ Toolbox issue tracker is just a click away (<a href="https://github.com/tlaplus/tlaplus/issues" rel="nofollow">https://github.com/tlaplus/tlaplus/issues</a>) and - since today - even has a UX label.
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.
Have any cloud providers or open source projects started publishing their proofs of correctness yet?<p>Is it cheaper to hire someone who knows TLA+ or to find a consultant?
Sorry, I still am wobbly on the matter of how TLA+ is different from QuickCheck and it's clones?<p>The idea that "you don't test a use-case, you test many inputs that may work differently" is solved by fuzzing/test factories.<p>So TLA+ without the fuzzing, leaves what, temporal stuff? Did I miss anything?