It seems to me that TLA+ is executable in the sense that a difference equation can be run forward in time. Plenty of mathematics is executable in that sense.
Specification is not the same thing as implementation. A specification language does not tell a machine what operations to perform, a programming language does.
System behavior and systems programming are entirely different uses of the word system.
> A specification language does not tell a machine what operations to perform, a programming language does.
There is a style of programming (usually functional or relational programming) that does not bother itself with operations, and which aims to merely describe a result. Specifications are still different from implementations written in such a style of programming.
And I would agree, TLA+ as a specification is different from TLA+ as an implementation. I generally disregard specs, I was talking about TLA+ the implementation when I said it had no future. It seems it will be in perpetual maintenance mode with barely any new features.
Regarding simple vs. easy, I challenge you to argue that temporal logic is "simple" in any sense of the word.
Almost spit out my drink dude, no jokes this early in the day.
That doesn't mean that it's easy, or easier, or that it feels more familiar to a programmer. These are different things.