An idea for teaching formal methods better

Teaching with pseudospecs

I was recently commissioned by a company to make a bespoke TLA+ workshop with a strong emphasis on reading specifications. I normally emphasize writing specs, so this one will need a different approach.

While working on it, I had an idea that might make teaching TLA+— and other formal methods— a little easier.

Pseudospecs

There are two problems to reading a spec:

1. Learning the mental model of what TLA+ is actually doing
2. Learning how to actually read TLA+.

The second problem is way, way bigger than it seems, because TLA+ has immense expressive power packed in a scary-looking syntax. Like take this spec:

---- MODULE foo ----
CONSTANT Servers
VARIABLE counters

Init ==
    counters = [s \in Servers |-> 0]

Zero(s) ==
    /\ counters[s] > 0
    /\ counters' = [counters EXCEPT ![s] = 0]

Inc(s) ==
    counters' = [counters EXCEPT ![s] = @ + 1]

Next ==
  \/ \E s \in Servers:
      \/ Zero(s)
      \/ Inc(s)

Spec == Init /\ [][Next]_counters
====

What's /\? What's ![s]? What's [][Next]_counters? To understand this spec, I have to understand how to read TLA+. This isn't an insurmountable obstacle, because otherwise nobody would know TLA+, but it could be the difference between "10 people learn TLA+" and "7 people learn TLA+".

My idea is to provide the spec along with a pseudospec, which could look like this:

Params {servers}

Initialize with {
   counters: Map(s in Servers: 0)
}

action Zero(s) {
    requires {
      counters[s] > 0
    }
    counters[s] := 0
}

action Inc(s) {
    counters[s] +:= 1
}

action Next {
  pick some s in Servers and { 
    either do Zero(s)
    or     do Inc(s)
  }

(Still working on what to do about the Spec operator.)

Couple things to notice. One: it's not a consistent translation between two languages, but between language and meaning. There's no formal grammar for the pseudospec. I need inconsistency for reasons I'll talk about later.

Two: the translation is not purely local. Things get moved around a little bit. Zero being an action affects how I translate \E.

Three: the translation is kind of metaphrasic. It's close to, but not exactly, a line-by-line translation. A person who has both files open in a split can correlate the spec and pseudospec.¹

Most directly, this will help people understand what the spec is doing, which gives me a basis to teach model-checking, safety properties, etc. But I think this will also makes learning the TLA+ syntax easier, by acting like an answer sheet. The student can read the TLA+ and, if they get stuck, look at the pseudospec for meaning.

My moonshot hope is that this also helps with writing specs, by giving people a clearer sense of the standard TLA+ idioms. I can translate the same syntax slightly differently depending on the way it's used, and whether it's a general construct or one for just the spec. That might be doing too much with this concept, though.

Problems I see

First is that there's lots of nuances that would be lost in the translation. In writing

Init ==
   /\ x \in 1..5

-->

Initialize with {
  x: pick some in 1..5
}

I lose the idea that Init isn't special, it's just a boolean operator like anything else. The student will have to unlearn that misconception if they ever need to do tricks like FastInit.

This is an essential tradeoff in pedagogy: is it better to teach the full picture now or the easy thing first and fix the misconception later? The teacher side of me knows that the white lie is better in the long run, but the expert side of me hates this.

Second, not every TLA+ symbol has a 1-1 mapping with English. I did the translation

\E s \in Servers:
  \/ Zero(s)
  \/ Inc(s)

-->

pick some s in Servers and { 
    either do Zero(s)
    or     do Inc(s)
}

That's because Zero and Inc are actions— things that update state. If they were regular operators, If P and Q are regular operators, I'd translate it like this:

exists an s in S {
   P(s) || Q(s)
}

Depending on the context, I'll translate \E in two different ways.

This ties back to problem #1. In TLA+, these are the same thing. Performing an action is literally saying that it's a true description of the next-state relation. This has the consequence of looking like it updates the state relation, but that's only in certain (exceptionally common) circumstances. This is all incredibly elegant and intuitive to a TLA+ expert, but not for a beginner. So I have to introduce some inconsistencies.

Problem #3 is just how much syntax I'll need to translate. What do I do for [A -> B], WF_vars, or \AA? I can try to avoid them for the early specs but can't do that forever.

Overall, though, I think the potential benefit of easier learning will outweigh the drawbacks.

Will this work?

We'll find out!

If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.

My new book, Logic for Programmers, is now in early access! Get it here.