Hacker News Reader

Comment by sesuximo | Hacker News Reader

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.

View on HN

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

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

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?

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.

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

Reply on news.ycombinator.com