On a type of TLA+ contract

88 views
Skip to first unread message

Andrew Helwer

unread,
Jul 4, 2025, 1:29:03 PMJul 4
to tlaplus
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:


Andrew Helwer

Andres Carignano

unread,
Jul 4, 2025, 2:01:29 PMJul 4
to tlaplus
Hello Andrew,

I'm a first year student in computer science and I work as a web programmer. Lately I've been looking into Leslie Lamport's papers and video lectures because I want to deepen my knowledge and skills in programming and mathematics. I've been wondering: what stops TLA+ from generating C style code? Is this a design decision or a technical obstacle? Maybe my question is incredibly basic, if so I apologize, my journey just begins. Maybe you can point me in the right direction.

Best regards,
Andrés Carignano.

Irwansyah Irwansyah

unread,
Jul 4, 2025, 6:04:12 PMJul 4
to tla...@googlegroups.com
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
--
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@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/76851a09-632a-4b93-9e5c-96dfbfa9dc21n%40googlegroups.com.

Andrew Helwer

unread,
Jul 4, 2025, 6:10:42 PMJul 4
to tla...@googlegroups.com
Hi Irwan, what do you mean by there being no incentive to open the knowledge to the public?

On Fri, Jul 4, 2025 at 4:04 PM Irwansyah Irwansyah <irwa...@gmail.com> 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...@gmail.com> 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:


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+u...@googlegroups.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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CA%2BKOs4z7AZzXn5P35ehhd6OGGx1ZA9ykj6FxN74L5H-rtEWrBQ%40mail.gmail.com.

Irwansyah Irwansyah

unread,
Jul 4, 2025, 6:14:33 PMJul 4
to tla...@googlegroups.com
Hi Andrew,

That is just my hypothetical question to find the root problem. Forgive me if it is incorrect.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@googlegroups.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@googlegroups.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@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUVz7aT57aS1imCJ9PwgEcNKeawrJneRh7aFSriTbDpHYA%40mail.gmail.com.

Finn Hackett

unread,
Jul 4, 2025, 6:53:09 PMJul 4
to tla...@googlegroups.com
I think Irwan's comment is about many industrial TLA+ specs not being made available, so no-one writes about them, making it harder to gauge who uses them and/or use those examples to become a new TLA+ contractor.

That said, it's not like there are no industrial-scale specs out there. Here are some I know about:
Of course I'm not a contractor (at least the way we mean it here), and none of these were open sourced from contract work (research orgs and open source contribs mostly). So, perhaps Irwan's point stands when it comes to contract work. Just wanted to share some actual production-scale examples that are available right now. Maybe they are an under-used teaching resource, if someone wanted to / had time to make heavily annotated versions of these specs, showing how they are structured and how to work with them.

Best,
-Finn

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.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+u...@googlegroups.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+u...@googlegroups.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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CA%2BKOs4y8PTTO7EgNaP%3DT8NMAJZ6fgBAvrQOJkFZ%2BZ9iFBp5pcA%40mail.gmail.com.

Hillel Wayne

unread,
Jul 8, 2025, 3:29:11 PMJul 8
to tla...@googlegroups.com
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 <irwa...@gmail.com> 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...@gmail.com> 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:


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+u...@googlegroups.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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CA%2BKOs4z7AZzXn5P35ehhd6OGGx1ZA9ykj6FxN74L5H-rtEWrBQ%40mail.gmail.com.

Arthur Daniels

unread,
Jul 8, 2025, 4:38:30 PMJul 8
to tla...@googlegroups.com
I am early in my TLA+ journey and look forward to becoming proficient. I am grateful for the generous contributions of the community from which I can continue learning. I fully believe in the benefits TLA+ can deliver. I am not a developer, but have many friends who are.

Speaking with them, I believe they conceptually feel TLA+ is a great idea, but fail to realize the direct benefit to their project given the upfront investment in learning TLA+ and extensive upfront planning. I get the feeling there's sometimes pressure to get results delivered quickly and TLA+ presents an investment in time that runs counter to that.

The issue as I understand it is not the benefit that TLA+ can deliver, the resources available or otherwise. I feel the issue is the demonstration that the benefits that TLA+ can deliver justify the investment in learning and continuous usage where appropriate.

Perhaps the issue raised by Andrew is not specifically around the terms or structure of the contract, but moreso how could a TLA+ expert implement it's continuous usage into an organization; demonstrating it's value and changing development processes to include its implementation wholesale within the organization at the very beginning.


Just an idea, a consultant business model could be organizational training, root and branch system checking for consequential bugs in its current state, and perhaps system reconfiguration/optimization accordingly.

Best, 


On Fri, Jul 4, 2025, 18:04 Irwansyah Irwansyah <irwa...@gmail.com> 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...@gmail.com> 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:


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+u...@googlegroups.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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CA%2BKOs4z7AZzXn5P35ehhd6OGGx1ZA9ykj6FxN74L5H-rtEWrBQ%40mail.gmail.com.

Irwansyah Irwansyah

unread,
Jul 8, 2025, 10:51:14 PMJul 8
to tla...@googlegroups.com
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

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAJ-b8sxUadf16sQRWZjw6oK%2BZx7Zki1f4vcjwfFA3%3D6yb3w-NQ%40mail.gmail.com.

Andrew Helwer

unread,
Jul 9, 2025, 12:41:12 PMJul 9
to tla...@googlegroups.com
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

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CA%2BKOs4yHHE2G5y6Dh0drhdZRm128Wo%3DyHy2n7TZQBfvNdMRbQg%40mail.gmail.com.

Andrew Helwer

unread,
Jul 9, 2025, 12:49:42 PMJul 9
to tla...@googlegroups.com
Re: Arthur Daniels' message:

Just an idea, a consultant business model could be organizational training, root and branch system checking for consequential bugs in its current state, and perhaps system reconfiguration/optimization accordingly.

That is probably true, and closer to the model that Hillel Wayne uses for his contracts (running TLA+ workshops).

Andrew

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAE7247um8Dd0ZKSiM7xNt3gmXPqdFNt13%3D6eGV4o3Xsn0MqB-A%40mail.gmail.com.

Irwansyah Irwansyah

unread,
Jul 9, 2025, 3:36:35 PMJul 9
to tla...@googlegroups.com
Hi Andrew,

Your answer reflects your vision on the future of TLA+. I don't know what your vision really is because I don't have the information but I suppose you agree that a vision is important if we want to achieve something.

In a product world, there is this notion of product vision (https://www.svpg.com/product-vision-vs-mission/). To achieve  the vision we need product strategy (https://www.svpg.com/product-strategy-overview/). I don't know what is the product  vision of TLA+ also what is the strategy. But I am "the customer" of the product (TLA+) and I have given my feedback (https://www.svpg.com/discovery-feedback/) and now it depends on "the people" behind the product whether to take the feedback or not.

Quoting Marty Cagan:
"If you are not regularly (weekly) actively seeking critical negative feedback, then I hope you take a few minutes with your team at your
next opportunity to discuss this. Ask yourselves if you are willing to change that, at least as a test, and then discuss the best way to go about it.

While your ego might get bruised a bit, I am fairly certain that you and your product will emerge much better for it."

Irwan

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUW1sur6B1PuVEVMK0LhFm84rcVdSh5r5sZzdPnK2iS0Xw%40mail.gmail.com.
Reply all
Reply to author
Forward
0 new messages