> Is TLA+ simple? I find this hard to accept.
It is very, very simple, and I would say easier to learn than Python, as long as you remember that it is not programming but maths. For example, suppose you specify this function on the integers:
f ≜ CHOOSE f ∈ [Int → Int] :
∀ x ∈ Int : f[x] = -f[x]
What function is it? Clearly, it's the zero function rather than what defining the equivalent "programming function" in, say, Haskell would mean:
f :: Integer -> Integer
f x = -(f x)
> Mathematics is not executable, though, whereas TLA+ is.
It is definitely not executable (i.e. not any more than mathematics is; you can specify executable things in maths and therefore in TLA+, but not everything you specify is executable). You can specify non-computable things (e.g. it is trivial to specify a halting oracle) as well as things involving real numbers. Moreover, when you check a TLA+ specification with a model-checker like TLC, it doesn't actually execute the specification, as it can check a specification of uncountable many executions, each of infinite length in a second.
However, you can certainly write formulas specifying the behaviour of an executable program and simulate it with TLC. But this is because you can use mathematics to describe physical systems, but not everything you can describe in mathematics can have a physical representation.
> "specification of system behavior" sounds like a programming language to me. A systems programming language, even.
A program is, indeed, one way of specifying a system, and TLA+ does allow you to specify an algorithm in this way (because maths allows you to specify programs), but it also allows you to specify systems in very useful ways that are very much not programs. For example, you can specify a component that sorts things without ever writing an algorithm for sorting, which is useful when the details of the sorting algorithm are irrelevant to the questions you want to answer. It's like how you can write a formula that treats planets as point-masses if you're interested in orbital mechanics, yet specify the earth in a much more detailed way if you're interested in predicting the weather.
> even as the language appears nowhere on the TIOBE rankings.
It is not a programming language. While it is true that far more people write programs than use mathematics to reason about physics, biology, or the way software systems behave (especially complicated interactive and distributed systems, which is where TLA+ excels), that doesn't mean such disciplines have no future.