Unambiguous lexical indicators for state variables

[shonfeder]

As we discussed in our meeting today, we should be able to perform static analysis to ensure that operators or expressions that only accept state variables are not misapplied.

I contend that making this a syntactic check will give the best bang for the buck :)

Discussed in #374

^{Originally posted by shonfeder November 27, 2022}
Closely related to the discussion about actions in #207

Problematic

In TLA, (state) variables are state functions:

A variable x is a state function -- the state function that assigns the value s〚x〛 to the state s.

Understood from the perspective of the programs specified by a TLA formula, state variables correspond to globally visible mutable regions of state. However, a programmer familiar with sateful programming (which includes Haskeller's: they just have the discipline to quarantine their stateful sub-programs) will be led astray if they try to think of the state variables as mutable values within the context of a TLA spec (see #372 (comment)).

I don't know of a good, precise analog to the semantics of state variables within a TLA formula in any widely used programmings language I'm familiar with. A trick with Prolog DCGs for "Implicitly passing states around" is the closest thing I can think of.

Given the central importance, relative strangeness, and many gotchas of TLA state variables, they may be a good candidate for use of syntactic salt.

Motivation

1. We think it will help reason about specs if all state variables are visible at a glance, and identifiable purely locally, without having to refer back to the initial declaration of variables.
2. Having a clear lexical differentiator allows us to trivially enforce that <- can only be used directly on state-variables (and not, on references to them, e.g., passed in through operator parameters).
3. Adding a less familiar symbol will remind readers and writers of specs to consider these names in a special light.

Concrete syntax proposal

An option we've discussed is to add a distinctive lexical marker to all state variables. The concrete syntax suggested by @bugarela is prefixing variables with a @. iirc, this is inspired by Ruby's use of @ for class instance variables.

Translating an example from one of our example specs, this proposal would look like the following:

  var @board: int -> (int -> str)
  var @nextTurn: str // who goes next

  action Init = all {
    @nextTurn <- "X",
    @board <- 1.to(3).mapBy(_ => 1.to(3).mapBy(_2 => "_")),
  }

  def BoardIs(coordinate, player) =
    @board.get(coordinate._1).get(coordinate._2) == player

  action Move(player, coordinate) = all {
    BoardIs(coordinate, "_"),
    @board <- @board.set(
      coordinate._1, 
      @board.get(coordinate._1).set(coordinate._2, player)
    ),