Hacker News Reader

Comment by geertj | Hacker News Reader

My current thinking on model checking (still evolving):

Modeling languages are useful to check the correctness of an algorithm during development. During development, a model can also serve as a specification for the actual implementation. This requires that your the modeling language is readable to a broad range of developers, which TLA+ is not. We have been experimenting with FizzBee (fizzbee.io) which looks promising in this regards.

When you go to prod, you really want to test your actual implementation, not a model of it. For this you want something like https://github.com/awslabs/shuttle (for Rust), or https://github.com/cmu-pasta/fray (for Java). Or use something custom.

View on HN

TLA+ has its own quirks, you could add sugar here and there, but from semantic standpoint you couldn't do much. It's "unreadable" because requires some mental model most of developers don't have. My point: you either provide "simple" tools which could do nothing for real models or they become on same level of "unreadableness" really fast.

It is in deed tricky, but we tried. We fully kept the semantics of TLA+, so the same mental model people still need to learn (at least a little), but a syntax that is much more familiar to engineers/programmers.

This is Quint [1], a different syntax for TLA+ with some extra tooling (type checker, CLI, evaluator, REPL, VSCode extension, testing framework, etc) which can be transpiled to TLA+ (which is a very direct translation, as the semantics is the same [2]) and therefore make use of the TLA+ tools as well (mainly the model checkers).

I think this is far from the same level of "unreadableness" than TLA+, and it makes formal methods much more approachable. It would be great if you could take a look and tell me whether you agree.

[1]: https://quint-lang.org/ [2]: https://quint-lang.org/docs/lang

I did an eval of Quint about year ago and did not find it compelling. It constantly refers to TLA+ and doesn't bring much benefits except typing. Syntax tries to cover underlying fact that state machine is expressed in terms of logic and math using "understandable" for programmers concept but it's very leaky in the end. IMHO "assign" is quite hard to grok without TLA experience. Documentation is scarce.

The most frustrating part it's hard to use with TLA+ background. I know how to do something in TLA but have no clue with Quint because translation rules aren't direct and obvious.

On the other hand it's a way better than PlusCal!

But I'm heavily biased. Please take this "critique" as a mumble from TLA+ initiated duckling.

Thanks for the feedback! We actually improved the documentation a lot in the last year, and we host it in a website now: [1]

Most of the documentation doesn't mention TLA+ anymore, as it is focused on new programmers coming to formal methods with no prior experience with it. I agree it was very confusing before!

Other than that, if I can argue against some of your points: 1. Quint brings more than just type checking (better IDE diagnostics, better REPL, better CLI, and runs that work like tests) [2] 2. The translation rules between Quint and TLA+ are actually very straightfoward [3], specially if we stay in the common idiom of TLA+. 3. This is more subjective, but a few people using Quint have reported to really like isolating the state machine into the "action" mode and then defining the protocol in "pure def"s. I understand what you mean by "leaky" and a part of me agrees with that, but, in practice, we are seeing real benefits on this side.

Again, thank you for your points - there's some stuff in your feedback I haven't heard before, and it's great to have a new perspective.

[1]: https://quint-lang.org/docs/language-basics

[2]: https://quint-lang.org/docs/faq#how-does-quint-compare-to-tl...

[3]: https://quint-lang.org/docs/lang

wow this is great!

do you cover all of that TLA can do??

TLA syntax is simply a pain to type on my keyboard and it has been a hurdle for the longest time...

I taught a lot of people TLA+ and while there's definitely essential complexity, a nontrivial amount is just syntactic friction. Consider

    \A x \in set: x.id /= 1 /\ ~x.active

    all x in set: x.id != 1 && !x.active

The latter has the same semantics but is much easier to read for the average developer, and more importantly is easier to type without syntax errors.

I agree, latexisms in TLA are on eye brow level of weirdness. Lesser punctuation syntax is always better.

That is literally what is holding me back every single time I get back to TLA+. I love your book and posts and always use it as reference to get back into it, but most of that "getting back" is just trying to remember all the minutia of the syntax. I wish there was simply a transpiler from some common syntax into TLA+. I don't even need Pluscal for the most part, and I'm fine with the concepts of temporal logic.

out of curiosity, how did you get comfortable with temporal logic? i’ve had a hard time finding good resources aside from H. Wayne’s stuff on TLA+

I found "Specifying Systems" by Lamport, and the examples it gives, to be an excellent introduction and a stricter companion to https://learntla.com.

It has some chapters that give very precise definitions of how things work in TLA (both on a language level as well as model checking), which answered some questions I often had along the way in more informal introductions.

You can also use Model-Based Testing (MBT) and produce (arbitrarily many) tests for your production code from your (model-checked) model.

Reply on news.ycombinator.com