[Mathnerd314]

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.

[erichocean]

> Math is a natural language

Almost spit out my drink dude, no jokes this early in the day.

[epgui]

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.

[Mathnerd314]

ChatGPT does just fine with math. I wasn't joking...

[pistoleer]

What's the joke?