Hi H,
What's missing are:
1. What is a formal spec and what's the difference with the implementation?
2. Programming model. Most engineers are already used to iterative programming models. If they have to pick up a pure functional language like Erlang, they have to change their current programming model to adopt a declarative programming model. This is not easy, because they need to change their habits. Same goes from regular ASP to ASP.Net, DOS based language to Visual Basic, etc. What programming model do they need to adopt to solve problems using TLA+?
3. There is no thorough documentation of TLA+ built in operators and constructs, I have to switch back and forth between Avalache docs, old.learntla+.com, etc to try to understand the constructs.
4. PlusCalc is just noise. It is just adding more complexity and confusion for new people learning TLA+. In my opinion PlusCalc should be removed from TLA+ offering because it has no clear positioning and value proposition. To implement a non concurrent algorithm in PlusCalc is harder compared to using Python. To implement a concurrent algorithm in PlusCalc, people need to understand regular TLA+ concepts first. So it is easier to just use regular TLA+ directly.
5. How to apply TLA+ in regular day to day mainstream problems which is integration between systems? What kind of abstraction is enough to solve the current problems? How can TLA+ speed up their development process?
6. How to write invariants, liveness, constraints, etc?
I am more than willing to help structuring the docs and knowledge to help new people (including me) acquiring TLA+ skill.
Irwan