Re: [tlaplus] On a type of TLA+ contract

Hi Irwan, regarding PlusCal:

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.

I do agree with your comparison of PlusCal to Python for pseudocode of non-concurrent algorithms (a topic I explored here) although will note that PlusCal still has value if you want to formally prove the algorithm correct - something which cannot be done in Python. TLA+ has its formal proof language & semantics which enable you to do this.

Beyond that, I do think PlusCal is quite useful. It is a good exercise to try to write a spec of an algorithm with nontrivial cyclomatic complexity (lots of if-statement branches, loops, etc.) in raw TLA+ to see how much easier PlusCal makes such things. On a personal level I do like TLA+ better than PlusCal and learned TLA+ first, like yourself, but people seem to find one easier than the other in a way that cannot be predicted.

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.

I agree this is a problem and we are trying to figure out how to solve it. Documentation is fragmented across several half-complete places. Probably the docs.tlapl.us wiki will be used, breaking down documentation according to the diataxis system. Fundamentally writing technical documentation is just a large amount of work, which will certainly need to be done, but a lot of things need to be done. However I agree it should be prioritized. There is of course a risk that the work fizzles out part-way and we are left with yet another partly-complete documentation fragment.

The rest of your points I find a bit hard to draw lessons from, because to my perception they are answered by existing tutorials. Every tutorial I've seen includes an overview on the difference between a specification and implementation, and how to write invariants and liveness properties.

Andrew

On Tue, Jul 8, 2025 at 7:51 PM Irwansyah Irwansyah <irwansyah@xxxxxxxxx> wrote:

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

On Wed, Jul 9, 2025 at 2:29 AM Hillel Wayne <hwayne@xxxxxxxxx> wrote:
Hi Irwan,

If you don't mind me asking, what's missing from www.learntla.com that prevents it from matching your criteria?

H

On Fri, Jul 4, 2025 at 5:04 PM Irwansyah Irwansyah <irwansyah@xxxxxxxxx> wrote:
Hi Andrew,

I believe the root questions need to be answered are:

Why a company have to asked you for the short term contract?

Because, they don't have staff that knows TLA+.

Why they don't have the staff?

Because TLA+ engineer is hard to find

Why TLA+ engineer is hard to find?

Because it is hard for non math person to learn TLA+

Why it is hard for non math person to learn TLA+?

Because there is no complete and easy to read books teaching TLA+ in real world usage?

Why there is no complete and easy to read books teaching TLA+ in real world usage?

Because there is no incentives to open the knowledge to public

Why there is no incentives to open the knowledge to public?

Because...

Irwan

On Saturday, July 5, 2025, Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:
Hi all,

I wrote a post on a type of TLA+ contract I've done a few times, why it never worked out as well as hoped, and what could be changed so future contracts see more success:

https://ahelwer.ca/post/2025-07-04-tla-contracts/

Andrew Helwer

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/76851a09-632a-4b93-9e5c-96dfbfa9dc21n%40googlegroups.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CA%2BKOs4z7AZzXn5P35ehhd6OGGx1ZA9ykj6FxN74L5H-rtEWrBQ%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAJ-b8sxUadf16sQRWZjw6oK%2BZx7Zki1f4vcjwfFA3%3D6yb3w-NQ%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CA%2BKOs4yHHE2G5y6Dh0drhdZRm128Wo%3DyHy2n7TZQBfvNdMRbQg%40mail.gmail.com.