3 ms·

Tla also introduces a new type of bug: differences between your tla model and your program. And I found that in order to get tla to reason about large programs

Tla also introduces a new type of bug: differences between your tla model and your program. And I found that in order to get tla to reason about large programs, you had to express the model in ways that look very different from the program. This issue alone is enough to dissuade me from using tla.

mhh__ 5y ago
But the whole purpose is to check your model before you write code, no? I get that differences are hard but it's better than nothing
colanderman 5y ago
I never recommend TLA for reasoning about programs, but about models. It's great for describing a system you're still designing.
- rramadass 5y ago
  Elaborate please; Without reasoning about programs how do you come up with the predicates which constitute a Model? Are you making a distinction between declarative logic used in specifications vs. say predicate transformers used in proving program correctness?
pron 5y ago
That's like saying that tests introduce a new kind of bug -- behaviours that aren't explored at all -- and that that serious issue (and it is, indeed, extremely serious) should dissuade you from writing and running tests. All software quality tools are imperfect, and even in the very few special cases where software can be realistically verified end-to-end, the behaviour of the actual system -- which also depends on hardware that can never be fully assured -- is not guaranteed. The only question that matters when evaluating a software quality tool is: does it improve the software's quality for a cost that is lower than achieving the same improvement by other means? In other words, does it save us money and/or pain? For TLA+, the answer in many cases is absolutely yes. I.e. there is no better/cheaper/easier way to gain the same benefit.
wtetzner 5y ago
The alternative is to not check the model at all. Doesn’t really seem better.

mhh__ 5y ago

But the whole purpose is to check your model before you write code, no? I get that differences are hard but it's better than nothing

colanderman 5y ago

I never recommend TLA for reasoning about programs, but about models. It's great for describing a system you're still designing.

rramadass 5y ago
Elaborate please; Without reasoning about programs how do you come up with the predicates which constitute a Model? Are you making a distinction between declarative logic used in specifications vs. say predicate transformers used in proving program correctness?

pron 5y ago

That's like saying that tests introduce a new kind of bug -- behaviours that aren't explored at all -- and that that serious issue (and it is, indeed, extremely serious) should dissuade you from writing and running tests. All software quality tools are imperfect, and even in the very few special cases where software can be realistically verified end-to-end, the behaviour of the actual system -- which also depends on hardware that can never be fully assured -- is not guaranteed. The only question that matters when evaluating a software quality tool is: does it improve the software's quality for a cost that is lower than achieving the same improvement by other means? In other words, does it save us money and/or pain? For TLA+, the answer in many cases is absolutely yes. I.e. there is no better/cheaper/easier way to gain the same benefit.

wtetzner 5y ago

The alternative is to not check the model at all. Doesn’t really seem better.