Usability feedback from modelling Interchain Security

[p-offtermatt]

I recently ported the Interchain Security TLA+ specification from @Kukovec to Quint. This worked fairly well and was a successful endeavor so far.

Previously, I also attempted to replicate the difftest model https://github.com/cosmos/interchain-security/blob/main/tests/difference/core/model/src/model.ts (a reference implementation of ICS in Typescript) in Quint. This attempt was aborted, as it turned out this was more difficult than anticipated.

I want to collect some painpoints I had while working with Quint:

• Error messages from the parser for effect mismatches are hard to digest. For example, error messages for effect mismatches look like this:

Expected [runningValidatorSet,outstandingPacketsToConsumer,outstandingPacketsToProvider,receivedMaturations,maturationTimes] and [outstandingPacketsToProvider,receivedMaturations,maturationTimes,outstandingPacketsToConsumer] to be the same
Trying to unify entities ['runningValidatorSet', 'outstandingPacketsToConsumer', 'outstandingPacketsToProvider', 'receivedMaturations', 'maturationTimes'] and ['outstandingPacketsToProvider', 'receivedMaturations', 'maturationTimes', 'outstandingPacketsToConsumer']
Trying to unify Read[v1121] & Update['runningValidatorSet', 
....

I'd suggest prefacing the messages by printing the variables that occur in one but not the other. Without such a diff, it's very hard to spot which variables differ among eg 10 variables that appear in both. It's also challenging to see which side of an action is which here, though I suspect that is harder to solve and I don't have a concrete suggestion how to display this better.

• The parser seems to hang sometimes - I had to restart VSCode a few times to get it to restart. I unfortunately didn't keep a concrete example, so this might not be very helpful, but I occasionally got the parser to just stop doing things. This might be a VSCode problem, I had that with other tools, too, but with the Quint parser it happened every couple of hours.

• When there is an error in the file, I had the experience that the parser becomes unreliable for the whole file.
  For example, when I wrote an action half-way, realized I needed to change something else in the code to make the action work, and left an action half-written with a syntax error and tried to change some other code before continuing,
  completely unrelated parts of the code started giving error messages.
  This seems to be handled better by parsers for other languages, where typically errors somewhere in the code seem much more constrained to one location and you wouldn't expect e.g. a type mismatch in one class cause an unrelated error to pop up in another class.

• The hover tooltips are super helpful to see types and effects, but sometimes they don't show me what I'd expect.
  For example, in a block like this:

evidences.forall(evidence => true)

hovering over evidence showed me the definition of forall, when I would have expected to see the type of evidence.

• In the REPL, Is there a built-in way to get a dump of the whole state? Of course it's possible to define a val for it, but this seems like a common enough use-case that it would be nice to have it built-in.

• When testing, I sometimes got an assertion failure. In the REPL, is there a way to just rerun the part of the test until the failure automatically, so that I can take a look at the state? Of course I can rerun the action, but I might not hit the same failure. verbosity=5 is not sufficient for what I want, since it doesn't print the full state. Making a verbosity config that prints all the variables might also be a nice idea.

• A bit of a vague painpoint I had is the inherent 'modify-once' nature of Quint (this would also hold in TLA+, btw, nothing inherent to Quint here). When I tried to replicate the difftest model that is very close to the implementation, I ran into the issue that e.g. in EndBlock, the same data structure is modified multiple times, e.g. imagine the staking module processes a change in the validator set, but the slashing module also removes a validator. In a standard programming language, this is easy - just run the staking module EndBlock, then the slashing module EndBlock. In Quint, both of these would have to modify the same variable. Optimally, I'd want an EndBlock action in both modules, but since they can't modify the same variable, the workarounds are a bit weird - the best thing I came up with was splitting the logic for modifying the validator set out from the action and calling it separately, but this doesn't feel very nice to me, since now the "caller" is burdened by the logic of reconciling the different changes to the validator set. It might be nice to have an example that shows how to handle something like this, maybe similar to the 'protocol anatomy' showing some best practice for this.

======

Despite the pain points, I'm very happy to be using Quint instead of TLA+ for this - writing the language is a breeze most of the time, and reading it is a pleasure. If you have any questions about the writeup, please feel free to reach out - it's hard to precisely convert these things into words at times, so I'm happy to have a chat if it helps!

[konnov]

Thanks a lot for the detailed feedback @p-offtermatt! We will definitely process it into smaller chunks :)

[konnov]

I have converted this issue into a discussion, so it does not get lost in the sea of small issues.