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
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.)
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 :)
@dataclass
class Person:
balance: int
def wire(a: Person, b: Person, amount: int):
if a.balance >= amount:
a.balance -= amount
b.balance += amount
@pytest.mark.parametrize(
"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
[0]https://www.cosmicpython.com/ [1]https://www.learntla.com/intro/conceptual-overview.html
I ctrl+f'd the page and the expansion of that acronym, Temporal Logic of Actions is nowhere to be found.
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.
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.
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.
Bought the book, FWIW, and love it - but this will help me evangelize TLA+ with my employer and other groups!
The images don't render correctly on macOS safari (v 13.1.3). They are squished horizontally.
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