Yet another example that TLA+ is math, not programming

I've found that this approach often backfires and makes people lose interest in TLA+. Telling people "it's not programming" tells people they can't use their intuitions for programming, and that they have to be "good at math" to learn TLA+. Neither is true.

(Also, Haskell isn't my strong suite, but aren't those completely different statements? Haskell functions are closer to TLA+ operators, not TLA+ functions.)