TLA+ is executable in the sense of Prolog: there is an algorithm (the TLA+ implementation) that takes a TLA+ program and produces output. Most mathematics is not executable in this sense, you will have a very difficult time doing anything useful with the PDF's of published math papers. Math is a natural language, TLA+ is not.
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.
If you really take the time to carefully think it through... Math is a much more "natural" and "intuitive" language than nearly any programming language.
That doesn't mean that it's easy, or easier, or that it feels more familiar to a programmer. These are different things.
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.