Hacker News new | ask | show | jobs
by Certhas 659 days ago
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.
2 comments
epgui 658 days 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.

link
Mathnerd314 659 days 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.

link
erichocean 659 days ago
> Math is a natural language

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

link
epgui 658 days 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.

link
Mathnerd314 659 days ago
ChatGPT does just fine with math. I wasn't joking...
link
pistoleer 659 days ago
What's the joke?
link