Docs and tutorials

[shonfeder]

Let's use this discussion to collect notes on ideas that will help us write docs. Useful topics to make note of as they occur to us will include:

• Pedagogical approaches
• Good examples
• Important concepts
• Useful metaphors
• Likely gotchas
• References

[shonfeder]

tl;dr: An important concept to convey to engineers is that their intuitions about how a sequence of stateful expressions advances the state of a program generally don't apply to TLA specs. All the expressions in a spec specify relations between two state (pure computational expressions leaving that relation completely undetermined), and no expressions advance or mutate state in any way.

Programmers are used to stateful programs encoding an implicit temporal order represented on the 2 dimensional plane of a program's text. Most commonly, they reason about time advancing forward through the lines of a program. Given

1: let x = ref 1
2: let () = x := !x + 1
3: let () = assert (!x = 2)

Programmers can often assume a simplistic reading in which each line is a step forward in time, and correctly expect the assertion on line 3 to hold. Of course, the line-oriented temporal sequencing is a fiction: really time moves thru the order of evaluation of (stateful) expressions, and various control flow mechanisms show that the two dimensional view is inadequate to understanding the time of the program's execution. This becomes even more explicit in languages that internalize the management of state -- like Haskell and friends -- in which the order of state updates is derived entirely from the order of evaluation of the expressions that represent the state.

In TLA+ and TNT, we can maybe think of time moving along an unrepresented Z axis that is not represented in the plane of the program text at all (with the exception of our then operator or TLA+'s \cdot). Special operators -- like TLA+'s ', or TNT's proposed new/next keyword and our delayed assignment operator <- -- enable us to specify connections between two successive states.

[shonfeder]

Distilling this a bit more, I think the point to really emphasize for onboarding engineers might be this:

Contrary to what engineers are likely to expect from programming languages, evaluation of expressions in TNT never advance the state (arguably with the exception of then?): evaluation of expressions only determines values which can be used to describe the properties of, or relations between, states.

[shonfeder]

The several related confusions around state variables and actions explained by @plafer in his excellent feedback in #435 should be very helpful in illuminating some of the pitfalls here.

[shonfeder]

Something that @bugarela just explained to me that we should also note as helpful mnemonic: the types and value constructors for collections are capitalized (Set, Seq) and the types for scalar values are lower case (int, string).