Motivation and advantage of Quint

[michwqy]

I don't find an answer in the document, so I start a discussion hoping someone could help me. It looks like Quint is a syntactic sugar of TLA+ and can be translated into it. I'm a little curious if Quint has any other advantages or features over TLA+, besides being closer to programming languages in syntax and more user-friendly for beginners.

[shonfeder]

Hi, @michwqy! Thank you for starting the discussion.

The best place to look for existing documents that address this question would be our Design Principles. But I think it's great to have more situated discussions on this important topic.

Before addressing your question, let me remark in this:

It looks like Quint is a syntactic sugar of TLA+ and can be translated into it.

It is worth clarifying that Quint is an alternative surface syntax for expressing
the temporal logic of actions, rather than a syntax sugar for TLA+ in the way
that, e.g., PlusCal is. Quint can be transpiled into the idiosyncratic TLA+
supported by Apalache, but it is
not principally compiled to TLA+ in our current usage. Quint has two main
compilation targets at the moment:

• The Quint simulator, which enables interaction via the REPL and supports
  testing specs.
• The Apalache intermediate representation, which enables verification via Apalache (and transpilation
  into TLA+). Note that this functionality is not stable yet.

Now, to your question:

I'm a little curious if Quint has any other advantages or features over TLA+, besides being closer to programming languages in syntax and more user-friendly for beginners.

We definitely do aim for those two goals! Here are some of the additional value
propositions on offer with Quint:

• We have tried to design a syntax that is very easy to parse and analyze. This
  enables quick iteration and improvement on the language and it invites the
  development of supporting tooling. This design choice has enabled quick
  development of the following tools, in a relatively short time, and with a
  very small team:

  • Static type checking
  • Static effect checking (explained below)
  • A REPL
  • A testing framework
  • An LSP server
  • A VSCode plugin
  • Tools for literate programming
  • Documentation generation tooling
  • Integration with the Apalache model checker

  More tools and language extensions are planned. We also hope this invitation
  will be taken up by others who find quint useful :D

• Quint is statically typed. This lets us identify and eliminate certain classes
  of common specification errors before spending any time in model checking or
  simulation.

• Quint has a simple effect system. This lets us reason statically about some
  kinds of state updates, allowing us to catch another class of specification
  errors statically. This also allows us to partition the language into a pure,
  deterministic, composable fragment and an impure, nondeterministic fragment.
  We have found this helps us discipline our spec writing, and some on our team
  are hopeful about additional abilities this might unlock.

• The quint toolset is designed and built from the ground up to be a well
  behaved CLI tool that plays well with other developer tooling. This is an
  unassuming choice, but in our experience this has a high impact on "time to
  value". As an example, it is trivial to integrate execution and analysis of
  quint specs into a CLI pipelines.

Lastly, I'd like to note that most of the Quint devs are big fans of TLA+! We
aspire to have a mutualistic and collaborative relationship with the existing
communities involved with TLA :)

Please let us know if you have any more questions, thoughts, or ideas!

[konnov]

Hi @michwqy!

Thanks for asking this question. @shonfeder has already covered the large part of our motivation behind Quint. He did not mentioned our initial hypothesis though: It is hard to write a parser for TLA+ and, as result, it makes it hard for engineers to learn its syntax. Basically, we do not want to change the logic of TLA+ too much, but we are aiming at proving an alternative syntax for the logic of TLA+. One relatively major change is that we are using fold over sets and lists, instead of arbitrary RECURSIVE operators.

Another hypothesis that we are checking is whether there is a larger community of engineers who are not learning TLA+ just because of its syntax and lack of tool support that they find in the mainstream programming languages.

I have also presented some of these points in the talk at the TLA+ Community Meeting 2023. You can check the slides. Sure, the slides are not as helpful as seeing a talk. We will probably record a talk in the future.

[michwqy]

Thanks very much for your relies @shonfeder @konnov . I wll try to summarize it, because I'm not sure if I get it right.

Quint is a newly designed specification language expressing the temporal logic of actions, and it has own simulator and model checking tool. Although Quint can be transpiled into TLA+, there are some syntactic differences between Quint and TLA+.

Besides, after reading the slides mentioned by @konnov and the paper metioned in the slides, I have some other questions.

Question 1

As far as my personal learning and use experience is concerned, the use of symbolic model detection is faced with a dilemma. For systems with small variable range (or behavior scale), symbolic model checking is significantly slower than explicit model checking. For systems with an unbounded (at least very large) range of variables (or behavioral scale), symbolic model checking is not as effective as testing methods based on satisfiability modulo theories (SMT) (like symbolic execution) or theorem proving. Symbolic Execution can customize the path search strategy and is closer to the programming language (or implementation). Am I right? Or any suggestions for the use of symbolic model checking.

Question 2

As mentioned in the slides, there are gaps between design ducuments, formal specification, and implemation codes. Quint provides a syntax closer to programming languages, reducing the gap between the latter two. Are there any other methods to reduce the gaps? Like making specification more easily updated with design or implementation updates. Or model-driven test/ model-based test?

Quint is an executable specification language

I originally thought this meant that Quint could not only be used for validation, but also be converted into programming languages for execution.

[Kukovec]

Hi @michwqy, I was going over the discussions and noticed that your questions went unanswered, so I hope it's not too late if I take a stab at answering them. For reference, I'm also an Apalache developer:

For systems with small variable range (or behavior scale), symbolic model checking is significantly slower than explicit model checking.

Depends on your definition of "significantly", but in terms of human-observable differences, for small examples, both approaches are basically instantaneous, in my experience.

... symbolic model checking is not as effective as testing methods based on satisfiability modulo theories (SMT) (like symbolic execution) ...

Symbolic model checking, at least in Apalache, IS SMT solving. Originally, people might have understood "symbolic model checking" to be BDD-based, but this is no longer common terminology.

Are there any other methods to reduce the gaps? Like making specification more easily updated with design or implementation updates. Or model-driven test/ model-based test?

Yes, primarily model-based testing. Quint and Apalache both utilize a common trace-representation format, called ITF, which can be consumed by other tools to basically drive a concrete implementation. There's actually a prototype tool that does exactly this, called Atomkraft

I originally thought this meant that Quint could not only be used for validation, but also be converted into programming languages for execution.

At present, we have no plans of supporting conversion to programming languages (e.g. Quint -> Python, Quint -> Rust or Quint -> Go, etc.). Quint is executable in the sense that it has its own simulator in Typescript, and REPL, that is, you can take a quint spec, invoke a function or action, and observe the result of the computation.