7 ms·

Simple =/= easy. 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

Simple =/= easy. 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.

Mathnerd314 2y ago
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 2y ago
  > Math is a natural language Almost spit out my drink dude, no jokes this early in the day.
  - Mathnerd314 2y ago
    ChatGPT does just fine with math. I wasn't joking...
  - pistoleer 2y ago
    What's the joke?
  - epgui 2y ago
    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.
epgui 2y ago
While I agree with you on the general idea, I think this is too restrictive: > 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.

Mathnerd314 2y ago

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 2y ago
> Math is a natural language Almost spit out my drink dude, no jokes this early in the day.
- Mathnerd314 2y ago
  ChatGPT does just fine with math. I wasn't joking...
- pistoleer 2y ago
  What's the joke?
- epgui 2y ago
  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.

epgui 2y ago

While I agree with you on the general idea, I think this is too restrictive: > 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.