Ideas for a user survey and language changes

[konnov]

@shonfeder and I discussed one more potential syntax change. Instead of creating another discussion on that, we thought that it probably makes sense to list small syntax changes in this issue. We could use these ideas to conduct a user survey later.

/cc @bugarela, @thpani, @Kukovec

[konnov]

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

[konnov]

Require

Another syntax feature is a decorator function like require(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

[konnov]

This surprisingly coincides with the discussion about pre/post-conditions in #892

[konnov]

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.

[konnov]

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 + y

def 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 though
def foo(x: int, y: int) => x + y
// always use the curly braces, this may introduce unnecessary nesting
def foo(x: int, y: int) { x + y }

[Kukovec]

Anyone who has passed primary school math class should be familiar with function definitions like this:

p(x) = x^2 + 2x + 1

[shonfeder]

I agree: i think we should just explain this in terms of equational reasoning (the lhs can always be replaced with the rhs, modulo substitution) and our users will understand. But this is something we can verify in the user study.

[konnov]

It's not about what people can learn. It's what may surprise people when they see it for the first time. Sure, people might have seen p(x) = ... at school, but = works differently in programming languages. It just occurred to me that I would subconsciously put parentheses in this definition:

def foo(x, y) = (x > 0 and y > 0)

Why does it happen? Perhaps, I am not sure about the priority of and and =. It's weird, but the symbol = causes some associations.

[konnov]

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, your MAX_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 that const are actually specification parameters. The same was happening in TLA+. I suggest that we simply change the const keyword to param, which better indicates that this name should be substituted with a value.

[thpani]

💯

[konnov]

Default values for specification parameters

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

module spec {
  const addr: Set[str]
  // the rest of the module
}

module spec3 {
  module I = 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.
  const addr: Set[str] = Set("alice", "bob", "eve")
  // the rest of the module
}

module spec5 {
  // this instance tests the specification for a larger set of addresses
  module I = instance(addr = Set("alice", "bob", "charlie", "eve", "fred"))
  // use the instance
}

[pdini]

Thank you Igor for cc’ing me. I confess that I don’t remember talking about this point, but I will keep it in mind since ASMs are very much function-based. Once the CoFi white paper(s) are done I will have more time to come back to specification. The idea of an CASM-Quint-CASM translation is still alive, even if not much progress has been made. I just spoke about it with Philipp Paulweber on Tuesday. To me it’s important because it’s the only way I will be able to learn how to make use of Quint properly, even though the TLA+ substrate does help understanding. Going on vacation from tomorrow until the 15th of August, back on the 16th. Perfect time for some theoretical thinking! :-) Cheers, Paolo

…

On 21 Jul 2023, at 09:48, Igor Konnov ***@***.***> wrote: This surprisingly coincides with the discussion about pre/post-conditions in #892 <#892> — Reply to this email directly, view it on GitHub <#608 (reply in thread)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA6HG24FG6TQK6ZOD3YSSG3XRIX6PANCNFSM6AAAAAAUQAOYOQ>. You are receiving this because you were mentioned.

[konnov]

No rush. I was just moving discussion around :)