Technology for higher-level syntax

[konnov]

Warning: this is a technical discussion exploring the solution space. If you would like to discuss concrete suggestions on the alternative syntax, it should not be done here.

Motivation

It became apparent in the discussions that the first users (mostly us) would like to have a higher-level syntax. For example:

• A more convenient combination of guess and <-: Introducing initializers #183 (comment)
• Some form of guarded commands: when (P) do { A1, A2, A3 }

We knew that this moment would come. The initial idea of Quint was that it could serve as a well-defined base-level syntax for other syntaxes. Among the Design principles of Quint are the follows:

• It uses a small set of syntactic rules.
• Most of the operators are mnemonic.
• It uses a small set of syntactic rules.
• We keep one-to-one correspondence with the most of TLA+ operators.

If we start extending the language with all possible syntax ideas, this will become a problem very quickly:

• The syntax will be bloated and it will be hard to support it at all processing passes.
• Some of the constructs proposed by the first users are incomplete, that is, they cannot completely replace some of the existing operators.
• We know that minimalistic syntaxes live longer than higher-level syntaxes. Examples are: LISP and SAL.

Problem statement

Instead of embedding all potential syntax constructs asked-for by the users, we need a syntax layer that is:

• Extendable. Either by us as the developers, or by the users.
• Isolated. It does not contaminate the rest of the Quint tooling.
• User-friendly. The users would like to see error messages that refer to the higher-level syntax, rather than messages that refer to the Quint operators.
• Recyclable. If we decide to throw away some of the experimental syntax, it should be easy to do.

Some points to understand:

• Does the syntax have to be extendable by the users? It may be sufficient, if we add the extended syntax rules. However, this would make the feedback loop slower.
• Can we make the syntax "isolated" and "user-friendly" at the same time?

Potential solutions

Two approaches immediately come to my mind:

1. Coq notation. It is a very nice and powerful mechanism. The users would be able to experiment with the syntax as much as they like. Unfortunately, it is not so easy to implement. We would need an extendable lexer and grammar. The current parser is done with antlr 4, which does not support extendable grammars. Perhaps, we could do that with Tree sitter, but that would require us to write another parser.
2. Hygienic macros. Here we have to understand how powerful these macros should be. The examples proposed by the users such as when (P) do { A1, A2, A3 } suggest that they would require us to extend the lexer and the parser to support these macros. Perhaps, we could limit the tokens to a set of predefined tokens (such as ,, ;, #, etc.) and limit the syntax rules used to defined macros to the rules from a subset of syntactic rules. To do that, we would have to collect a library of potential macros.
3. Another parser on top of the existing one. By extending the existing grammar, we could define a superset of Quint. We would simply translate the extended syntax rules to their base definitions in Quint. This should be sufficient for an MVP. This is also supported by ANTLR 4, see this discussion

[tesnimab]

My first thoughts about this preliminary analysis, especially the following statement:

If we start extending the language with all possible syntax ideas, this will become a problem very quickly:

The syntax will be bloated and it will be hard to support it at all processing passes.
Some of the constructs proposed by the first users are incomplete, that is, they cannot completely replace some of the existing operators.
We know that minimalistic syntaxes live longer than higher-level syntaxes. Examples are: LISP and SAL.

Let's not discuss vague possible syntax ideas and define them through concrete examples (The clock example to start with perhaps).
Given what we want to add, we evaluate the impact on existing Quint syntax and see if it brakes the mapping to TLA+ semantics.

If it does break the TLA+ semantics, evaluate to what extend ? and is it problematic?
If we choose not to change the Quint syntax and go for another solution, how much time do we need to implement it, and is it worth it given the amount of time already engaged and yet to be engaged on Quint.

Does the syntax have to be extendable by the users? It may be sufficient, if we add the extended syntax rules. However, this would make the feedback loop slower.

I think we are not in the stage we want users to extend the syntax. This is another topic that needs another discussion.

[konnov]

If it does break the TLA+ semantics, evaluate to what extend ? and is it problematic?

I would be very curious to see an example where TLA+ as logic is insufficient. It already contains first-order logic, the whole set theory (ZFC), temporal operators, and a bunch of convenience modules such as sequences, bags, etc. (which can be implemented in TLA+ itself). Given that, I would not like to engage in any long-term research on extending the logic of TLA+ without having a good evidence for that it is needed. Extending the syntax is a different thing. You do not have to break logic foundations to extend the syntax with convenient expressions.

As a quick example, we all know that $p \Rightarrow q$ is equivalent to $\neg p \lor q$ and $p \land q$ is equivalent to $\neg(\neg p \lor \neg q)$ in Boolean logic. We also know that $\neg p$ and $p \lor q$ build a complete base in Boolean logic. So we have $p \land q$ and $p \Rightarrow q$ for convenience in Boolean logic. We could say that the language of { $\neg, \lor$ } is the base language, whereas the language of { $\neg, \lor, \land, \Rightarrow$ } is its extended syntax.

Now, if for some reason we decided to replace $\lor$ with $\land$ in { $\neg, \lor$ }, we would be lucky, as we preserved completeness. However, if we decided to replace $\neg$ with $\Rightarrow$ in { $\neg, \lor$ }, we would make it incomplete. Note that extending { $\neg, \lor$ } with $\Rightarrow$ keeps the set of operators complete, as we can always fall back to $\neg$ and $\lor$, whereas $\Rightarrow$ is just a convenience operator.

[tesnimab]

So I don't see the problem of extending the Quint syntax if we are able to map it anyway to TLA+ without breaking the logic.
Again, I think we should discuss concrete examples, not taking decisions over assumptions, it may be simpler than it may seem.

[konnov]

I agree with you. This is why we are discussing the technological base here, not the concrete syntax extensions.

[thpani]

I think it's premature to discuss implementation details.
IMO, we should go with @Kukovec' route of doing user research first, then make design decisions, then discuss technology. (Of course, there will be some interaction between these elements to ensure what we're trying to do is actually feasible).

A few comments in response to the assumptions in the OP:

• It [Quint] uses a small set of syntactic rules.
• Most of the operators are mnemonic.
• We keep one-to-one correspondence with the most of TLA+ operators.

I think all of these must be seen relative to other design goals. In fact, they are all phrased in relative terms ("small", "most", ...).

If we start extending the language with all possible syntax ideas, this will become a problem very quickly:

• The syntax will be bloated and it will be hard to support it at all processing passes.

Adding syntax results in more syntax, not necessarily "bloated".
Choosing the wrong syntax may result in an unusable, bloated, or any kind of system.
It would be great if we could stay away from framing our concerns in biased terms.

I also think this is pure speculation, unless we have user research on the table with concrete syntax suggestions.

In fact, the suggestion for supporting outside <- binding with guess (#183 (comment)) is directly in response to Quint not allowing us to reference next-state variables. In a similar fashion, one could argue that the current syntax is bloated, because it does not allow us to refer to interesting terms without nesting them inside lambdas.

• Some of the constructs proposed by the first users are incomplete, that is, they cannot completely replace some of the existing operators.

Nobody asked to replace a complete set of operators.

• We know that minimalistic syntaxes live longer than higher-level syntaxes. Examples are: LISP and SAL.

I don't think there's any evidence for this claim.
Fortran has rather baroque syntax, is as old as Lisp, and remains very popular in scientific computing.

[konnov]

Putting this question on hold also makes sense. This is how we could do it without having requirements.

[konnov]

I think the main question here is how to get the feedback from the users about potential syntax extensions without having a concrete implementation. We will have the simulator to try the current syntax in action. So what Jure @Kukovec is also an approach to this problem.

[thpani]

On the technical side, I think layering multiple syntaxes has the downside of less integration:

• There might be things that we want to do in the high-level syntax tooling that are easier to achieve with direct access to the low-level tooling (tracking LOC for error reporting is a classic 😄 ).
• We'd have to maintain two sets of artifacts for the separate syntax layers.

In that sense, it's a classic cohesion vs coupling exercise :)

@konnov You seem to be very much on the side of least coupling here, even if it reduces cohesion.
I would definitely want to understand the perceived downsides of a more integrated approach first.

[andrey-kuprianov]

I agree. It is definitely much closer to the engineering practice than TLA+, but still a long way to go. So probably it's better not to advertise it as an easy to use modeling language for engineers, which it is not (simply because the basic concepts such as non-determinism are hard to grasp without training in formal methods). This is the task for the languages that we will build on top of Quint.

[konnov]

All of this is true, but we also communicated that Quint would be what engineers choose to write in.
It seems we're pivoting on this part.

OK. Let's see. One of the main features of Quint is the clear separation between stateless and stateful definitions, actions, and temporal formulas. So learning the stateless and stateful part of Quint should be real easy. It is basically a simple functional language.

The friction points come when we are talking about actions and temporal formulas. For temporal formulas, the engineers will have to learn them, there is no way around, but they will probably use temporal formulas in rare cases, so they are definitely not the first thing to learn.

When it comes to actions, we have four new primitives: <-, guess, &, |. I think it is not a lot to learn. However, as we have heard, we want to avoid the visual shock, when the engineers see a spec for the first time. So this is the main motivation for introducing higher-level syntax, which smoothes the experience, at least, in the beginning.

Finally, when we designed Quint, we had all kinds of engineers in mind. If we are pivoting to Cosmos blockchains, we are pivoting. Hence, we need a DSL on top of Quint. This is, again, not big news. I think we have discussed something like with @andrey-kuprianov 1-2 years ago.

[konnov]

On top of that, if somebody wants to use Quint to write smart contracts, we are really pivoting.

[thpani]

When it comes to actions, we have four new primitives: <-, guess, &, |. I think it is not a lot to learn.

I think you overlook the fact that many people don't know how to encode symbolic transitions as logic constraints. If one understands this concept, sure, Quint is easy to learn. If one doesn't, then & and | are hieroglyphs.

[konnov]

When it comes to actions, we have four new primitives: <-, guess, &, |. I think it is not a lot to learn.

I think you overlook the fact that many people don't know how to encode symbolic transitions as logic constraints. If one understands this concept, sure, Quint is easy to learn. If one doesn't, then & and | are hieroglyphs.

Oh yes. This is exactly we have isolated these four. In TLA+, everything is about logic constraints, and that is why it is quite hard to understand what is going on. I am actually quite happy that we did it, so that we can now have this discussion!

[konnov]

Adding syntax results in more syntax, not necessarily "bloated".
Choosing the wrong syntax may result in an unusable, bloated, or any kind of system.
It would be great if we could stay away from framing our concerns in biased terms.

I also think this is pure speculation, unless we have user research on the table with concrete syntax suggestions.

True. Extended syntax is not necessarily bloated. I just want to find a way to isolate extended syntax, so we do not have to deal with it at all stages of translation. In this sense the current Quint syntax is self-contained and complete. Also, it follows very simple principles at the moment, in contrast to the syntax of TLA+. It is not minimal in the logic sense, as we have KerA+ in Apalache, which is a much smaller language core.

[thpani]

I just want to find a way to isolate extended syntax, so we do not have to deal with it at all stages of translation. In this sense the current Quint syntax is self-contained and complete.

I'd say this is usually a feature you want from internal representation, not from user-facing syntax.

What's the benefit of having this minimal core language facing the user?

[konnov]

The truth is that Quint is the syntax of the internal representation of Apalache, and it looks much more consistent than the syntax of TLA+, due to its syntactic minimalism.

The immediate benefit is one-to-one correspondence with TLA+:

• For someone knowing TLA+, it's easy to see how to write Quint.
• The language semantics is immediate. It is the same semantics of TLA+.
• We know how to deal with this semantics.

Obviously, for someone who has never seen TLA+, the benefit is not obvious. My bet is that it will still be easier to learn Quint syntax than TLA+ syntax. But we can only learn that by doing a controlled experiment :)

[thpani]

Sure, I agree that current Quint will be easier to learn than TLA+.
I'm not contesting the benefits of Quint in its current form, I think there are plenty 🙂

I think the comments from Zarko, @tesnimab, @andrey-kuprianov and myself were in support of making it even easier to learn Quint without a background in TLA+.

[andrey-kuprianov]

I clearly see and agree with the intention to make Quint the basic language layer, on par with internal Apalache representation. And whatever constructs we want to build that provide ease-of-use, more compact syntax, domain-specific constructs, etc., can be done as specialized languages on the next levels. The next language levels would actually a subset of what's expressible in Quint, and the best way to go, as I see it, is probably via:

• providing syntactic translation of higher-level constructs into lower-level Quint, thus making the whole Apalache toolchain applicable to new languages, and giving the user the baseline solution that works always;
• possibly developing specialized model checking techniques for higher-level languages, which would work directly on the language representation, and may provide better performance

[konnov]

I mean, whether a higher-level language is a subset or a superset, it is a good question. For instance, TypeScript is a superset of JavaScript. This was a puzzle for me for a long time, but now I see what they actually mean by that :)

[bugarela]

(This is my current opinion on the matter after all conversations at the retreat and reading this discussion. I'm open to further discuss the matter.)

It doesn't make sense to me that we were discussing how we can become a standard in verification and, when it comes to Quint, we want everyone to define how they prefer to write it. I don't believe at all that syntax is only a matter of personal taste. My opinion in a very direct statement is: We can find the best possible syntax to define state machines, and then everyone should use this syntax instead of whatever they prefer. We can have libraries for specific contexts and even DSLs if we want to target very specific contexts, but macros for basic language constructs (such as when (...) { ... }) shouldn't be an option. Otherwise, I see us ending up with unrecognizable Quint specs all over GitHub that no one can understand anymore, and I'd really prefer to have standardization.

What I think we should have for starters:

1. Quint base language capable of specifying generic state machines.
   • As Jarko mentioned, we have room for improvement in terms of making specs better resemble a state machine. I think we should try that.
   • Even with the current syntax, I think anyone that knows what a state machine in CS means could understand Quint specs after reading a 5min tutorial on how transitions are defined with actions.
2. A library (or perhaps some DSL) specific for some cosmos use case.

In addition: we should not underestimate our team's capacity to determine what's better for Quint. We have some of the most experienced TLA+ users when it comes to real-world applications AND tool builders for the language. We know the problems we are trying to solve, while most users we would be able to interview at this point will not have a sense of the problem at all. I'd rather have user interviews regarding documentation and the VSCode plugin when those are in place.

[thpani]

Good summary, I agree on most points!

Just a few thoughts:

Even with the current syntax, I think anyone that knows what a state machine in CS means could understand Quint specs after reading a 5min tutorial on how transitions are defined with actions.

Sure; I think we're trying to bridge the gap between "can understand after reading docs" and "desperately wants to use" 🙂

In addition: we should not underestimate our team's capacity to determine what's better for Quint.

I think we're doing a good job here, in that we make it a team effort rather than a single person designing the language.

We have some of the most experienced TLA+ users when it comes to real-world applications AND tool builders for the language.

As I've said many times, I think this is also a considerable downside.
Many of the Quint design goals are centered around avoiding previous painful interaction with TLA+, rather than creating a useful general-purpose specification language.

most users we would be able to interview at this point will not have a sense of the problem at all

I think that's precisely the point:
If I show the average developer a code snippet in a not-too-obscure new language, they will usually have some intuition about what the code does – usually enough to read it (in general terms).
I'd like to see us reach a similar level of intuition for Quint, and we currently have few data points on what users find intuitive or not.

[andrey-kuprianov]

Hey @bugarela! I am quite enthusiastic about your approach:) I particularly like the close-to-my-perfectionist-heart statement like the below one :D

We can find the best possible syntax to define state machines, and then everyone should use this syntax instead of whatever they prefer.

I also tend to agree with

we should not underestimate our team's capacity to determine what's better for Quint. We have some of the most experienced TLA+ users when it comes to real-world applications AND tool builders for the language.

My main problem is that when we talk about state machines, we should clearly understand that there is not a single notion of a state machine, but rather at least 3 broad directions how state machines are described. In particular:

• State-based approach, of which a good representative is a Kripke structure. This approach focuses on a finite number of states, and transitions between them, and that's what most developers have in mind when they talk about state machines.
• Event-based approach (or language-based one), of which representatives are e.g. Regular expressions, CSP, or Event structures. They focus on sequences of events, and the formal language these sequences describe.
• Transition-based approach, of which representatives are Transition systems, the TLA+ itself, Z notation, ASMs. They focus on finite sets of transitions, and how to describe them.

Characteristic of those approaches is that many problems are naturally expressed in one approach, but come with substantial loss of compactness/expressiveness (sometime exponential) when translating from one approach to another one. Transition-based approach is kind of a common denominator of all others: they can be expressed in it, the complexity increase is not exponential, but the loss in understandability is still substantial. I see transition-based approach as an assembler of specification languages: everything can be expressed, but there are many more convenient approaches for specific cases.

To conclude: I do agree that we should build Quint as the best assembler language possible. And definitely much better than TLA+. But we should clearly understand that it still will be an assembler, and it can't embrace all possible higher-level approaches; it can only provide the basic layer into which they can be translated. In my view, Quint is going to be exactly the right input language for Apalache, but in 5 years almost no one is going to actually use it for writing specs: this is the task for the languages that will come after it.

[bugarela]

Hey @andrey-kuprianov, thanks for all the background, I did not have that classification in mind!

In my understanding of the project, the aim is to make Quint the language people use to write specs for distributed systems. We should evolve it to have really good UX, which is something we are spending most of our resources at the moment. It does not need to constraint itself to be the right input language for Apalache, and we are already deviating from that in some ways (as with 0-indexed sequences instead of 1).

Also, I don't think we need to support all these different ways to define state machines, as we can focus on the distributed systems scenario and stick with transition-based approaches.

[andrey-kuprianov]

yes, transition-based approach is good, and I like it (transition systems are my favorites): they are the most general ones, and many things can be expressed reasonably well. So I agree with the choice:) I am only pretty sure that this is not going to be the last step in the specification languages evolution, which is also a good thing: the evolution should not stop. In any case the step Quint is doing is a necessary (and long overdue!) one.

[tesnimab]

To resume, we have to move forward and try to bring the improvements to the pain points (& and | are not sufficient to describe a transition in the action and the behavior of the system in next can also be improved as mentioned in the discussion on Pluscal/TLA+/Quint) I agree that our goal is to have a useful general-purpose specification language not only an improvement of TLA+, only TLA+ people can sense. A lot of good work has been involved, I think we just need to be open in pushing the concept a little further not changing it. Shon is writing the spec for the clock example in Quint (it s the use case mentioned in the discussion). It's a starting point to come up with alternatives to address the pain points. We can see other examples too. From there we discuss the pros and cons and to-dos before jumping into implementation.

[konnov]

I agree that we should get feedback from the users. My concerns are:

• If we get feedback from a very small group of people (Ethernal), then this may be non-representative and lead to a big miss.
• If we get shallow feedback in the form "I did not try it, but I don't like how it looks", then we will be changing cosmetics instead of changing the pain points.

To avoid this, I see two complimentary ways:

• We have to design a user survey (better, if it lets people write things), get a large enough audience, conduct the survey, and gather the results.
• We should make interactive spec-writing sessions with several users and see where they are getting stuck. I have been doing essentially the second kind of observations with engineers when they were writing TLA+ specs, though I have not been doing that in a systematic way either.

These approaches are described in the usability literature. Maybe @designsingh could guide us a bit there.

[konnov]

Also, we should differentiate between the two scenarios:

• The first encounter. What we have seen as a very quick feedback that the action operators were surprising. The question is how to avoid that. It is not as trivial, as these are new concepts. Substituting them with other concepts, which we believe people already know, may help or may not help.
• Daily use. We have not tried yet how people are using the language in their work. It may happen that the cosmetics will get into their way in the day-to-day work. We all know that shiny consumer products are not always fun to use.

[tesnimab]

Of course, we will do the user survey and take into account the concerns you mentioned.
What we can do right now is proposing alternatives on the examples and we discuss them together internally first.