I shouldn't be so harsh on teaching TLA+ with puzzles

I know I'm getting the newsletter out very late this week (this kind of lackadaisical nonprofessionalism is why I don't offer paid subscriptions) so I'll keep this one short.

Over the past couple weeks I've seen a few TLA+ articles where people show how to solve the wolf-cabbage-goat puzzle. You know the one where you have a farmer who has to cross a river in a boat, but he can only take one item each trip, and has to keep the wolf from eating cabbage or the goat from eating a wolf?¹ It's a common example used to introduce formal methods it makes me worried that people'll think FM is only useful for solving toy puzzles. I prefer to teach with examples of real-world systems.

A similar example is the SEND MORE MONEY puzzle in all the constraint solving books: assign unique digits to letters such that SEND + MORE = MONEY. I've read books that had dozens of examples, all like this, and I was left wondering what I was supposed to do with constraint solving.

Anyway, I now think I'm being too hard on these kinds of examples. Two reasons for this. First, it provides more opportunity for practice. Getting good at these things takes time and work, and you need to understand the domain to model it. So practicing TLA+ on a bunch of puzzles might be easier than practicing on a bunch of real-world systems, since you don't need to spend as much time understanding the premises of a puzzle as you do a whole system. I noticed this while learning Picat: I did so in order to solve a practical problem, but I learned and practiced by writing Petri net solvers.²

Now the other reason is a little more philosophical: what makes computation interesting? "Computation" is not the same as programming. This is programming:

>>> print("hello world!")
hello world!

And this is programming that's also computation:

>>> 100**(1/17)
1.3111339374215643

Calculating the 17th root a number isn't something I can do myself, or even with a pocket calculator. But with a computer I can do it easily, as long as I know a programming language that makes it easy to express the computation. On the other hand, puzzles like wolf-cabbage-goat and SEND MORE MONEY are hard to express. If you want to solve them in Python, you'll have to write your own solver engine, and that'll take magnitudes more time than originally expressing the problem does.

So it's interesting that the TLA+ solution can be under 20 lines. It's shows that TLA+ can be used to compute things that ordinary programming languages cannot, at least not without a lot of extra programmer effort.

Learning TLA+ (or constraint solvers, or functional programmer, or whatever) expands the range of computations the user can easily do, and showcasing this with puzzles is a good way to demonstrate that. Just make sure to teach actual use cases too!

As penance for my prior grognardery, here's Tower of Hanoi in Picat:

import planner.

final({Rung1, Rung2, Rung3}) =>
  Rung1 = [], Rung2 = [], sorted(Rung3).

action(S0, S1, Action, ActionCost) =>
  Action = S1,
  ActionCost = 1,
  member(From, 1..3),
  member(To, 1..3),
  S1 = copy_term(S0),
  S1[From] = [H|T],
  if S1[To] != [] then head(S1[To]) > H end,
  S1[From] := T,
  S1[To] := [H] ++ S1[To].

main =>
  Start = {[1,2,3], [], []},
  best_plan(Start, 20, Plan),
  writeln(Start),
  foreach(Action in Plan)
    writeln(Action)
  end,
  nl.

Next week will have two newsletters as normal, and then I'll be on vacation until after Thanksgiving. Have a great weekend everyone!

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.