I haven't done any work on this since July due to needing to prepare a new TLA+ workshop from scratch, but now that that's over I plan to spend a day each week doing updates. On the docket:
- Moving some of the examples from Practical TLA+ over to the site
- Adding more exercises to the core
- Adding the new modules and TLC options showcased at this years TLAConf
- Way, way more examples and advanced topics. I have half a dozen pure TLA+ specifications on my computer I need to write up.
Just wanted to say that I think you single-handedly have made formal methods approachable to an order of magnitude more people (at least) than it was before.
TLA+ is much easier to get into than, say, Coq or Isabelle or something, but a lot of the "pre-learntla" content out there is still really mathey and scary for engineers to jump into. I think you did a really good job making TLA+ and PlusCal a useful tool for non-scientists. Thank you.
It would be quite easy for Coq or Isabelle to express the logic in a TLA spec, you're basically just adding a few modalities (time, state, non-determinism) over plain old boolean logic. Then you're free to use any of a number of tools (usually SAT/SMT solvers) to try and find a refutation of your spec. There really isn't a lot of complex math involved.
Yes, you could basically do anything that TLA+ does inside of Isabelle (more familiar with that one than Coq), but it's harder. I think what makes TLA+ interesting is that an engineer with basically no understanding of anything more complex than "I basically know what a set is" can be useful within an afternoon or two.
I love Isabelle but it's got a substantially steeper learning curve than TLA+. I'm not saying it's unnecessarily steep, because Isabelle is a lot more versatile than TLA+, but as a result it's a fairly difficult sell for employers, at least in my experience.
Love "Computer Things", and, tbh, forget sometimes that you and the "LearnTLA+ guy" are the same person; great work on both fronts, and thank you so much for putting posts/resources out there and contributing to these corners of the web; I'll be sure to check out LTLA+ when it & I are ready c:
One thing I really appreciate about your site is that you have a setup guide, with photos! This is really helpful for folks unfamiliar with how to run a spec.
- Moving some of the examples from Practical TLA+ over to the site
- Adding more exercises to the core
- Adding the new modules and TLC options showcased at this years TLAConf
- Way, way more examples and advanced topics. I have half a dozen pure TLA+ specifications on my computer I need to write up.