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?<p>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?<p>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 :)<p><pre><code> @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
</code></pre>
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?"<p>[0]<a href="https://www.cosmicpython.com/" rel="nofollow">https://www.cosmicpython.com/</a>
[1]<a href="https://www.learntla.com/intro/conceptual-overview.html" rel="nofollow">https://www.learntla.com/intro/conceptual-overview.html</a>