What's your recommendation on how to rapidly learn TLA+? I spent some time staring at references and the UI a few months ago and came away very defeated. But I'd like to actually level up here.
I also found TLA+ difficult to learn and a chore due to the syntax. I truly wish designers of popular languages would incorporate model verification within the language/compiler tools - this would likely need a constrained subset of the language with restricted syntax and special extensions. Ideally, it should be possible to just annotate or "color" a function for formal verification. All parameter types and functions used by the "formal" function would also be colored.
> I also found TLA+ difficult to learn and a chore due to the syntax.
This is a common complaint among beginners. The problem is that the syntax is very helpful later and, I would claim, is also helpful for beginners once something very important clicks.
TLA+ is a language for writing mathematical/logical formulas, and uses the standard mathematical/logical syntax that's developed over the past 150 years. There is no funamental reason why the standard symbol for conjunction (logical and) should be ∧, but that syntax developed so that ∧ is visually similar to ∩ (set intersection) because of the deep relationship between the two (a ∩ b = {x : x ∈ a ∧ x ∈ b}) which means that many transformations apply to both symbols in a similar way (same goes for the disjunction -- logical or -- symbol, ∨, and set union ∪, as a ∪ b = { x : x ∈ a ∨ x ∈ b}). As you learn to apply mathematical transformations on formulas, that syntax becomes helpful (not to mention that it's the same syntax you'd find in mathematics/logic texts where you can learn those transformations). On the other hand, the corresponding symbol used in programming, typically &, was chosen due to the technical limitations of computer input devices in the 1950s rather than as a means to aid the work of the programmer in some deeper way.
Now, the reason I would claim that the syntax is also helpful for beginners (although I acknowledge it is a "familiarity" stumbling block) is that it reminds them that the meaning of formulas in TLA+ is the same as their simple meaning in mathematics rather than their very complex meaning in programming. This is the important thing that needs to click into place.
For example, in mathematics, a function on the integers defined like so, f(x) = -f(x), has the meaning of being the zero function -- the function that is zero for all x. This is simple and obvious; to see that, add f(x) to both sides and divide by 2. Specifying a function in that way in TLA+ would specify the zero function. In few if any programming languages, however, would a function defined in this way specify the zero function. Usually it specifies something much more complicated, and that's because programming is much more complicated. There are many other such examples.
On the first day of a programmer learning TLA+, functions and operators may appear similar to subroutines in programming, but the similarity is superficial, and soon the big differences become apparent. The meaning of these things in TLA+ is much simpler than in programming and also much more powerful as they're more amenable to applying transformations and substitutions (e.g. in TLA+ there is no difference between x' = 3 and 3 = x', while the software operation this TLA+ equation often describes -- that of assignment -- behaves in a much more complicated way in code).
The mathematical syntax helps remind us that we're writing mathematics, not code, and that the symbols have their (simpler and more powerful) mathematical meaning rather than their coding meaning.
The purpose of TLA+ is to reason about the behaviour of a dynamic system in a rigorous way. That requires applying transformations (such as adding things to both sides of an equation, substituting things etc.), that, in turn, requires that symbols have their mathematical meaning, and that is aided by the standard mathematical syntax (again, not just because that syntax was often chosen to evoke important similarities but also because that syntax is the one that's used in most texts about logic/mathematics).
For me that clicked when I was learning TLA+ a decade ago and I asked on the mailing list if TLA+ uses eager or lazy evaluation. Leslie Lamport replied that there is no "evaluation" at all in mathematics.
> I truly wish designers of popular languages would incorporate model verification within the language/compiler tools - this would likely need a constrained subset of the language with restricted syntax and special extensions.
This is not so simple because the things you want to express about programs often goes well beyond what can be used to produce something executable, and, as I mentioned before, is aided by using mathematical meaning. There are languages that do what you want, but either their specification power is relatively weak (e.g. Dafny), or they're much more complicated than both TLA+ and mainstream programming languages (e.g. Idris).
TLA+ allows you to use a simple and very powerful language for the specification part and a relatively simple mainstream language for coding without compromising either one. The difficulty, however, is internalising that writing specification in TLA+ is a different activity from coding, and trying not to extrapolate what you know from code to maths.
TLA+ is actually much smaller, simpler, and easier to learn than Python, it's just that you need to understand that you're starting from scratch. Someone who doesn't know programming would learn TLA+ faster than Python, it's just that if you already know programming, learning a new programming language may be easier, at least at first, than learning TLA+ -- something that is very much not programming (even though it's simpler than programming).
> the "formal" function
"Formal" merely means mechanical, i.e. something that can be operated on by a computer. All programming is formal.
I would say that learning TLA+ is first and foremost learning how to describe systems using mathematics. It isn't at all as scary as it may sound, but it also very much isn't the same as describing a system in code.
You definitely don't have to learn to do that to use some formal verification tools, but that is what you commit to learning when you choose to learn TLA+ specifically. That is because the assumption behind the design of TLA+ is that using mathematics is ultimately the easiest and clearest way to describe certain important things you may wish to know about programs. TLA+ is a produce of the nineties, and the specification languages that preceded TLA+ in the eighties used more programming-like approaches. And TLA+'s novelty came largely from abandoning the programming approach. It is a later, rather than an earlier evolutionary step.
However, if you accept that you won't be able to describe such things, certainly not easily, then there are other languages and tools that don't require a mathematical approach -- some predate TLA+ and some are later, but follow the earlier approach of the 1980s.
