Notes from a newbie after doing the kettle tutorial

[plafer]

I thought I'd share my notes when taking the tutorial here; hopefully it can be useful for you to see what goes on in the mind of a newbie :).

1. Why is the ' necessary when assigning a var?

   • I understand from previous discussions that sometimes you need to refer to "before" and "after".
   • However would it not be possible to just have the ' syntax when that is strictly necessary? I'll let you be the judge of that!

2. Sections 5.2 & 5.3 were surprising to me:

   • creating the kettleState uses reference semantics; the syntax for me suggested value semantics (i.e. copying).
   • that is, val kettleState = { heatingOn: heatingOn, beeping: beeping, temperature: temperature } creates references to variables, as opposed to copying their state.
   • Perhaps a "reference-of" operator of some kind would eliminate the confusion?

3. The all {} expression used in actions combines pre-conditions, as well as "assignment statements" (which I assume evaluate to true).

   • would it be better to distinguish those? Specifically, it's not yet clear to me why it "makes sense" for an assignment statement expression to evaluate to bool (as opposed to, say, the value that was assigned, as in C).
   • although I currently suspect that this would make sense after I've learned the whole language and learned to "think in it".

4. I tried

>>> any { temperature' = temperature + 1, temperature' = temperature - 1 }
>>> kettleState
runtime error: <input>:4:1 - error: Variable heatingOn is not set
4: var heatingOn: bool
   ^^^^^^^^^^^^^^^^^^^

runtime error: <input>:5:1 - error: Variable beeping is not set
5: var beeping: bool
   ^^^^^^^^^^^^^^^^^

<result undefined>

4.1. Why do I need to specify how every variable changes? Would it be bad if TNT assumed that any unspecified change means "no change"?
4.2. heatingOn and beeping are unusable after this statement.

>>> heatingOn
runtime error: <input>:4:1 - error: Variable heatingOn is not set
4: var heatingOn: bool
   ^^^^^^^^^^^^^^^^^^^

<result undefined>

with no way to assign a new value to it.

5. About nondet temp = oneOf(-40.to(40)). Putting nondet before the variable name is confusing to me.

   • For me, this suggests that the variable is declared as "non-deterministic", whereas I understand this line as oneOf being non-deterministic, and temp to simply be an int that gets assigned the result of evaluating oneOf.

6. At the end of "5.5. Introducing data non-determinism", the explanation for the snippet

nondet myElem = mySet.oneOf()
expr

is:

REPL randomly picks one of the elements from the set mySet and binds the name myElem to the chosen value.

I initially read this as "the nondet syntax is a REPL-only feature". After re-reading the whole explanation, I realized that REPL here meant "the whole interpreter as used by the REPL program". In other words, for me, REPL means literally the "read-eval-print loop"; the program that reads user input, manages the history of commands, etc. Could this be reworded as:

The current implementation of TNT randomly picks one of the elements from the set mySet and binds the name myElem to the chosen value. Other implementations might do it differently.

General feedback

All in all, I agree with Ethan that this was delightful 😉. With no prior background, I was able to follow easily and get a feel for TNT. The feel of the REPL was also great; reminded me of ipython!

[shonfeder]

1. Why is the ' necessary when assigning a var?

The ' refers to a state variable in the next state, and the assignment is what we've called a "deferred assignment", that is: it refers to the variable in the next state. The priming is meant to help make it clear why the following is true

all {x == 1, x' = 2, x == 1}

under the assumption that this alternative formulation without the prime would be confusing:

all {x == 1, x = 2, x == 1}

However would it not be possible to just have the ' syntax when that is strictly necessary? I'll let you be the judge of that!

I think we can say that it is strictly necessary any time you are specifying the value of a state variable in the next state, which is the case for all "assignments" :)

WDYT? Any ideas on how we could make this clearer?

[plafer]

I'm still digesting all this information, but I can already say:

WDYT? Any ideas on how we could make this clearer?

Reading your note was very insightful! I definitely think after state variables are introduced, there should be some text explaining how to reason about "assignments".

[shonfeder]

creating the kettleState uses reference semantics; the syntax for me suggested value semantics (i.e. copying).

State variables refer to regions of state. This is a fundamental concept that takes a bit of time to grasp. But one way to think of this is that, in the context of the simulator, state variables are ref cells. Or, equivalently, the value of a state variable is a function of the current state. As you change the state (by applying actions) their value will change.

So kettleState is actually value semantics, you cannot mutate the record it is assigned to. Only the values of each record field in this case are state variables, and those have reference semantics :)

Perhaps an aside or a link in the REPL tutorial to the basic concepts for state variables would be useful?

[plafer]

So the kettleState record here

>>> val kettleState = { heatingOn: heatingOn, beeping: beeping, temperature: temperature }

would be in C

// The KettleState record state holds constant pointers to mutable data
struct KettleState {
    bool *const heatingOn;
    bool *const beeping;
    int  *const temperature;
} 

right? Then in C, to initialise a KettleState struct, we would write

bool heatingOn;
bool beeping;
int  temp;

struct KettleState k = { &heatingOn, &beeping, &temp };

These are familiar concepts in "imperative programming" (in a very hand-wavy way), except with different syntax. My confusion stemmed from the fact that TNT syntax resembles "imperative languages syntax", except it seems "value semantics syntax" is used for reference semantics... Unless there's still something I'm misunderstanding.

Perhaps an aside or a link in the REPL tutorial to the basic concepts for state variables would be useful?
Yes definitely, an explanation of how to think about all this would be very useful.

[shonfeder]

3. The all {} expression used in actions combines pre-conditions, as well as "assignment statements" (which I assume evaluate to true).

There's been some prior discussion on separating out preconditions from "updates" and in general on exploring alternative syntax for actions. See #207 if you're interested in giving input on any of the ideas we've been kicking around :)

it's not yet clear to me why it "makes sense" for an assignment statement expression to evaluate to bool (as opposed to, say, the value that was assigned, as in C).

This is because x' = 3 means "the value of the state-region x in the next state will be 3". It is stating a constraint that holds over the next state, and it is true or false based on whether the region of state named x can actually have that value in the next state.

I think this point touches on a key conceptual shift that differs from the usual programming languages, which I've tried to elaborate a bit here #372 (comment)

No obligation, but I'd be interested to know if any of this helps clarify, or if we are still missing the mark when it comes to explaining the shift in thinking on this point.

[shonfeder]

About nondet temp = oneOf(-40.to(40)). Putting nondet before the variable name is confusing to me.

• For me, this suggests that the variable is declared as "non-deterministic", whereas I understand this line as oneOf being non-deterministic, and temp to simply be an int that gets assigned the result of evaluating oneOf.

This is a great point and connects with an ongoing debate over nondet 😄 (In case you're interested, that discussion is mostly now at #398.)

[shonfeder]

6. At the end of "5.5. Introducing data non-determinism", the explanation for the snippet

This is a good point. I've tried to making a fitting change in #436

[shonfeder]

4. I tried

>>> any { temperature' = temperature + 1, temperature' = temperature - 1 }
>>> kettleState
runtime error: <input>:4:1 - error: Variable heatingOn is not set
4: var heatingOn: bool
  ^^^^^^^^^^^^^^^^^^^

runtime error: <input>:5:1 - error: Variable beeping is not set
5: var beeping: bool
  ^^^^^^^^^^^^^^^^^

<result undefined>

4.1. Why do I need to specify how every variable changes? Would it be bad if TNT assumed that any unspecified change means "no change"?

In general, we have in mind a mechanism for this, but there is some subtlety and I think the discussion is not totally settled.

4.2. heatingOn and beeping are unusable after this statement.

>>> heatingOn
runtime error: <input>:4:1 - error: Variable heatingOn is not set
4: var heatingOn: bool
  ^^^^^^^^^^^^^^^^^^^

<result undefined>

with no way to assign a new value to it.

Did you try heatingOn' = true? This is working for me. Assuming I understand the scenario you're describing, here's a minimal reproduction:

>>> var x: int

>>> var y: int

>>> val r = {x: x, y: y}

>>> r
runtime error: <input>:0:1 - error: Variable x is not set
0: var x: int
   ^^^^^^^^^^

runtime error: <input>:1:1 - error: Variable y is not set
1: var y: int
   ^^^^^^^^^^

<result undefined>

>>> x' = 1
true
>>> x
1
>>> y' = 2
true
>>> y
2

Please let know if I'm missing the point here!

[plafer]

heatingOn and beeping are unusable after this statement.

I think I just got confused that setting a variable in the repl unsets the other ones. I probably did the equivalent of:

>>> x' = 2
true
>>> y
<error>

and concluded that there was a TNT bug 😅

[shonfeder]

Yeah, this connects with your question around how we handle variables whose next state is not specified. Anytime an action is applied (and in this case it includes updating a single state variable), the state moves forward, and -- currently -- unless the value for a variable in the next state has been specified, it becomes undefined.

We do need to figure out how to help shape or reflect intuitions around this stuff, as it is quite different from people's expectations coming from stateful languages :D

[shonfeder]

Your excellent questions have inspired some ideas on how we can support intuition formation in the REPL. I wonder if looking at the mockup there might even help refine your intuitions? #446

[plafer]

Thank you for the helpful responses @shonfeder! I'll aggregate my current understanding & suggestions in this one comment here.

It seems like conveying the "state machine" + "delayed assignment" semantics is a core issue. I think I understand the issue at hand here, and I still don't see why it couldn't completely be modeled in the "traditional imperative syntax". Here's how I would design the syntax; hopefully this is helpful input into the whole syntax discussions, or at least would just shed light on what I'm still confused about.

I would have a TNT "module" be similar to a Java class. By that I mean that "global variables in the file" are implicitly defined as state variables, and methods in the file are your actions. That is, actions map from state to state, and methods can do just that. Preconditions are assert() statements at the top of the method; post-conditions are assert() statements at the bottom. A rough sketch of a file would be:

// These are the state variables, accessible as `this.variable` in methods
var temperature: int
var heatingOn: bool
var beeping: bool

// This is the "constructor" of my state
func init() {
  this.temperature = 20
  this.heatingOn = false
  this.beeping = false
}

func pressButton() {
  // preconditions go here under an "assert" statement
  assert( not(this.heatingOn) )
  
  // It could be an error to assign the same state var twice
  this.heatingOn = true
  this.beeping = false
  // temperature is unchanged, so no need to "reassign" it

  // post-conditions would go here as "assert" statements
}

// *other methods go here*

func step() {
  // "select" is the equivalent of "any"; taken from go's channels' `select`
  // There is probably better syntax for this; my current view of this is I'm
  // passing functions to an operator that calls an arbitrary one
  select {
    this.pressButton,
    this.heat,
  }
}

With this syntax, we still get the "normal assignments", and I don't think there would be any confusion as to whether I'm using the "pre-state" or "post-state" of a variable, as discussed here. An alternative "API" would be to have methods return "Self", which would have a more functional feel.

Now I don't have the whole context/experience of writing specs to know if this is actually a good idea, but hopefully this take on solving a few problems I've experienced can help in any way.

[shonfeder]

@plafer Thanks for sharing the ideas! I think we've been kicking around some related ideas in the discussion around #207.

global variables in the file" are implicitly defined as state variables, and methods in the file are your actions

This is roughly what we currently, with the exception that we differentiate between different kinds of methods depending on their effect, i.e., whether they update or read state at all.

Let me ask you a followup: With the syntax you've proposed, what value would you expect this.beeping to end up with after pressButton has been applied, if we defined the operator as follows?

func pressButton() {
  assert( not(this.heatingOn) )
  
  this.heatingOn = true
  this.beeping = not(this.heatingOn) // <<<< NOTE THE CHANGE
}

[plafer]

I see your point, and understand better the challenge with using imperative-looking syntax.