41d ago
My mind works best with examples, I was about to ask here when I stumbled upon it on the TLA site [0].

The example starts out with a simple piece of code that exposes a bug, then the bug gets fixed and the following question is asked:

> Does the issue go away because we’ve solved it, or because we’ve made it rarer? Without being able to explore the actual consequences of the designs, we can’t guarantee we’ve solved anything

> The purpose of TLA+, then, is to programmatically explore these design issues. We want to give the tooling a system and a requirements and it can tell us whether or not we can break the requirement. If it can, then we know to change our design. If it can’t, we can be more confident that we’re correct.

[0]: https://www.learntla.com/intro/conceptual-overview.html

I wonder if it's possible to model how fucked up the Golang concurrency model is with TLA+?

As a TLA non-SME I couldn't say, but would definitely find it useful and probably impressive. Maybe Brad Fitzpatrick could team up with Aphyr and use it to make golang v2 a bit less crap.

Note: I write this with love, as someone who's written hundreds of thousands of lines of Go, and am now turned off and afraid of the behavior at the sketchy edge boundaries. I've now shifted to learning Rust, albeit slowly and finding it saddeningly challenging compared to what I can pump out with the Go.

For reference, see "Data Race Patterns in Go", posted 21 days ago: https://news.ycombinator.com/item?id=31698503

I just started reading the book a couple of days ago. Sigh... :-)

One thing that I wish websites did is to make it easy to report simple typos and grammatical errors without having to go through GitHub. For example, on https://www.learntla.com/intro/faq.html "losting" should be "losing". It would be great to simply and quickly report them without having to context switch and go through the overhead of opening an issue or creating a PR. (In any case, I don't even have a GitHub account.)

Genuine question: how does this compare versus something like modelling in primitive python? what benefits are there, or is it just a case of age and that this is language / system agnostic?

I'm just finishing cosmic python[0], which talks about making a primitive model of your system first, that you can run business logic tests on, then all the other code depends upon that (domain driven design / onion layers, etc). To me it seems like this is the same thing. The only aspect that stuck out was the "two transfers at the same time" which to me, seems like it would depend on how you're implementing the model, rather than the model itself?

For instance, the example in [1] could also be done in primitive python, (arguably easier to read in my opinion but I'm not used to TLA syntax :)

    class Person:
        balance: int

    def wire(a: Person, b: Person, amount: int):
        if a.balance >= amount:
            a.balance -= amount
            b.balance += amount

        "a_amount, b_amount, transfer, a_remaining, b_remaining",
            (10, 10, 10, 0, 20),  # matching amount
            (6, 10, 10, 6, 10),  # has less
            (0, 10, 10, 0, 10),  # has nothing
            (10, 0, 10, 0, 10),  # to empty account
    def test_wire(a_amount, b_amount, transfer, a_remaining, b_remaining):
        a = Person(balance=a_amount)
        b = Person(balance=b_amount)
        wire(a, b, transfer)
        assert a.balance == a_remaining
        assert b.balance == b_remaining
The author did mention "... could be done in python" as well, so I doubt it's a case of not knowing about python, but perhaps my question is "why TLA over python?"

[0]https://www.cosmicpython.com/ [1]https://www.learntla.com/intro/conceptual-overview.html

So can it spit out C or something? Or something to actually perform the algorithm? Or are you expected to manually translate back and forth between your model specification and your code?
Several people I know with a formal methods and distributed systems background aren't that impressed with TLA+. I'm not exactly sure why or what else they prefer (Isabel? Coq?). Anyone with a formal methods background care to comment?
Ah, the HN's favourite language Three Letter Acronym +

I ctrl+f'd the page and the expansion of that acronym, Temporal Logic of Actions is nowhere to be found.

I wish sites like these were keyboard operable. You have a link down the bottom of the page, if I scroll to the bottom of the page (with space or down key or page down), it would be nice that it gets to the bottom, and then goes to the next page on the next keydown event.

We implemented this in medical software for reading patient documents at one of my last jobs, and it's a feature I wish more sites that were focused on reading material had (docs, book replacements, etc.)

Edit: just want to point out this is in no way a critique of this site specifically, so maybe off topic.

Really liked the paper book, looking forward to the new version of the website!

Nice to see some new posts on TLA every once in a while. A few days ago someone posted this series of very real-world examples: https://elliotswart.github.io/pragmaticformalmodeling/ It's also quite good.

This looks like it could be really useful. I tend to write out my specs in pseudocode before coding anyway, so being able to easily translate that human gobbledygook into a form that can be checked for correctness, seems like it could help the creative process of coming to a solution. Just try out ideas and see if they help solve it. Keep honing them down until you get it.
Thanks for your work, Hilel! I've been using TLA extensively in my job the last few months (I work at a blockchain company), and it's been a good run - we found a bunch of issues in several designs and even implemented code (some fairly critical). My secret hope is to get some co-workers to start using TLA themselves (so I can go off to do code-level verification instead hehe), I've organized a couple of internal tutorials but no takers so far - hopefully this free learning resource will help advance that goal :)

On a related topic, does anyone know of a comparison to Alloy 6? I've been meaning to take a day or two to look at it (I tried Alloy out a while ago while I was still in my PhD, but have forgotten most of it), I'm curious to see how it stacks up.

Congrats Hillel, great work. A teammate used TLA+ at work to help diagnosis a deadlock bug due to a lock issue in postgres, and since then I've been mesmerized by its simplicity and power to prove simple invariants over complex specs. Looking forward to reading more!
Awesome, thank you, Hillel!

Bought the book, FWIW, and love it - but this will help me evangelize TLA+ with my employer and other groups!

This is good stuff, Hillel. Thank you.

The images don't render correctly on macOS safari (v 13.1.3). They are squished horizontally.

How does TLA compare to Spin?
This is very interesting and practical. Thank you.
I wish this wasn't so focused on PlusCal
any examples of where TLA+ is being used? do any open source projects use this?
This looks awesome. I'm hoping to start working through it starting some time in the next few weeks.