Converted this to a discussion, as they allow for nested comments.

Require

Another syntax feature is a decorator function likerequire(cond) that could make it easier for Solidity readers to understand preconditions. Instead of writing:

all {  (x < 10),  x' = x + 1}

We could write:

all {  require(x < 10),  x' = x + 1,}

See a comment:https://github.com/informalsystems/quint/pull/596/files#r1094462558

Optional terminator for val

https://github.com/informalsystems/quint/pull/596/files#r1094481184

action mint(sender: Addr, receiver: Addr, amount: UInt): bool = all {    require(sender == minter),    val newBal = balances.get(receiver) + amount    all {        ...

@Kukovec expected a ',' in the end of line after val.

Equality in definitions

We have received early feedback that the the equality sign in operator definitions may look surprising, e.g.:

def foo(x, y) = x + ydef foo(x: int, y: int): int = x + y

We don't know the exact reason for this, but this syntax may indeed look surprising to people who worked only with imperative languages before.

There are two alternatives to the current syntax:

// using lambda-like syntax, this may be surprising to FP people thoughdef foo(x: int, y: int) => x + y// always use the curly braces, this may introduce unnecessary nestingdef foo(x: int, y: int) { x + y }

The keyword for specification parameters

This is a comment by@pdini:

What is the difference between a pure value and a const? The reason I ask is that in ASMs they are both static functions, where the const is a 0-ary static function. Interestingly, yourMAX_UINT is a 0-ary static function, but you call it a pure value rather than a const. Therefore, there must be some difference between these two constructs that I do not see yet.

It is not the first time that we have to explain thatconst are actually specification parameters. The same was happening in TLA+. I suggest that we simply change theconst keyword toparam, which better indicates that this name should be substituted with a value.

Default values for specification parameters

In the current syntax, we simply specify constants and expect the user to define the constants values withinstance. For example:

module spec {  constaddr:Set[str]// the rest of the module}module spec3 {  moduleI= instance(addr=Set("alice","bob","eve"))// use the instance}

This approach is nice and general, but this makes the simplest use cases a bit too complicated. The beginners have to remember that
they need to define an instance, just to start testing. We want the users to start testing their spec as soon as possible, when they are writing the spec. In the early stages, we have received feedback that it would be good to have default values for variables. I am not sure about the state variables, but having default values for constants now makes sense to me. I remember that@bugarela mentioned something like that too. We could introduce default values. Engineers would probably set them to meaningful examples. Specification purists would probably set them to the most general case. In any case,instance would let us override the values of the constants. For example:

module spec {// The address is set to the three-element set by default.// This spec is executable and testable right away, without the need for instance.  constaddr:Set[str]=Set("alice","bob","eve")// the rest of the module}module spec5 {// this instance tests the specification for a larger set of addresses  moduleI= instance(addr=Set("alice","bob","charlie","eve","fred"))// use the instance}