The Future of TLA+ [pdf] • Hacker News Board

Re: The Future of TLA+ [pdf]

#11

Post by colanderman » Wed, Aug 28, 2024, 8:21 PM UTC

Mathnerd314 wrote: post #9

> Simplicity is a major goal of TLA+. Is TLA+ simple? I find this hard to accept. > TLA+ isn’t a programming language; it’s mathematics. Mathematics is not executable, though, whereas TLA+ is. > TLA+ [is better] for its purpose than a programming language. "TLA+ is a formal specification language designed by Leslie Lamport for the specification of system behavior." "specification of system behavior" sounds like a pro…

TLA+ is only "executable" in the same sense that an algebraic expression is executable. It's perfectly possible to write things on TLA+ that can not be simply executed linearly. (These overlap to a great extent with the things which TLC rejects.) As a basic example, it's easy to write a statement with \A (unbounded universal quantification) whose truth can only be judged by a proof engine.

Specification languages are explicitly not programming languages, for the core reason that programming languages dictate only what must occur; whereas specification languages can dictate what must not occur. It's not possible with a "specification" written using a programming language to determine what of a program is actually the specification, vs. what is an accident of the implementation.

Re: The Future of TLA+ [pdf]

#12

Post by tailrecursion » Wed, Aug 28, 2024, 8:22 PM UTC

Mathnerd314 wrote: post #9

> Simplicity is a major goal of TLA+. Is TLA+ simple? I find this hard to accept. > TLA+ isn’t a programming language; it’s mathematics. Mathematics is not executable, though, whereas TLA+ is. > TLA+ [is better] for its purpose than a programming language. "TLA+ is a formal specification language designed by Leslie Lamport for the specification of system behavior." "specification of system behavior" sounds like a pro…

> "specification of system behavior" sounds like a programming language to me. A systems programming language, even.

Lamport has directly and repeatedly addressed the differences between what's desirable in a specification language versus what's desirable in a programming language. Understanding the difference is vital to writing specifications.

Re: The Future of TLA+ [pdf]

#13

Post by Certhas » Wed, Aug 28, 2024, 8:23 PM UTC

Mathnerd314 wrote: post #9

> Simplicity is a major goal of TLA+. Is TLA+ simple? I find this hard to accept. > TLA+ isn’t a programming language; it’s mathematics. Mathematics is not executable, though, whereas TLA+ is. > TLA+ [is better] for its purpose than a programming language. "TLA+ is a formal specification language designed by Leslie Lamport for the specification of system behavior." "specification of system behavior" sounds like a pro…

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.

Re: The Future of TLA+ [pdf]

#14

Post by lolinder » Wed, Aug 28, 2024, 8:27 PM UTC

threatofrain wrote: post #2

A TLA+ alternative people might find curious. https://quint-lang.org/

Previously discussed: https://news.ycombinator.com/item?id=41111790

Re: The Future of TLA+ [pdf]

#15

Post by candiddevmike » Wed, Aug 28, 2024, 8:28 PM UTC

max_ wrote: post #5

westurner wrote: post #3

Earlier quoted context omitted.

What are other limits and opportunities for TLA+ and similar tools?

Limits of TLA+ - It cannot compile to working code - Steep learning curve Opportunities for TLA+ - Helps you understand complex abstractions & systems clearly. - It's extremely effective at communicating the components that make up a system with others. Let get give you a real practical example. In the AI models there is this component called a "Transformer". It under pins ChatGPT (the "T" in ChatGPT). If you are to…

Are there any RFCs written in TLA+?

Re: The Future of TLA+ [pdf]

#16

Post by lolinder » Wed, Aug 28, 2024, 8:34 PM UTC

Mathnerd314 wrote: post #9

> Simplicity is a major goal of TLA+. Is TLA+ simple? I find this hard to accept. > TLA+ isn’t a programming language; it’s mathematics. Mathematics is not executable, though, whereas TLA+ is. > TLA+ [is better] for its purpose than a programming language. "TLA+ is a formal specification language designed by Leslie Lamport for the specification of system behavior." "specification of system behavior" sounds like a pro…

> even as the language appears nowhere on the TIOBE rankings.

TIOBE rankings are widely considered to be useless by those who care about programming languages, but even aside from that your dismissal on those grounds is absurd given that you had just barely criticized TLA+ for trying to duck the label of "programming language" at all. You can't criticize it for trying not to be a programming language and then turn around and criticize it for not showing up on a ranking of programming languages.

It's excluded from the TIOBE index in the same way that HTML, CSS, or Markdown are excluded, and that's by choice.

Re: The Future of TLA+ [pdf]

#17

Post by fiddlerwoaroof » Wed, Aug 28, 2024, 8:36 PM UTC

skybrian wrote: post #8

max_ wrote: post #5

Earlier quoted context omitted.

Limits of TLA+ - It cannot compile to working code - Steep learning curve Opportunities for TLA+ - Helps you understand complex abstractions & systems clearly. - It's extremely effective at communicating the components that make up a system with others. Let get give you a real practical example. In the AI models there is this component called a "Transformer". It under pins ChatGPT (the "T" in ChatGPT). If you are to…

Is that a practical example? Has anyone specified a transformer using TLA+? More generally, is TLA+ practical for code that uses a lot of matrix multiplication?

The most practical examples I’m aware of are the usage of TLA+ to specify systems at AWS: https://lamport.azurewebsites.net/tla/formal-methods-amazon....

Re: The Future of TLA+ [pdf]

#18

Post by koolala » Wed, Aug 28, 2024, 8:41 PM UTC

max_ wrote: post #5

westurner wrote: post #3

Earlier quoted context omitted.

What are other limits and opportunities for TLA+ and similar tools?

Limits of TLA+ - It cannot compile to working code - Steep learning curve Opportunities for TLA+ - Helps you understand complex abstractions & systems clearly. - It's extremely effective at communicating the components that make up a system with others. Let get give you a real practical example. In the AI models there is this component called a "Transformer". It under pins ChatGPT (the "T" in ChatGPT). If you are to…

Sounds similar to UML: Unified Modeling Language diagrams.

I wonder if TLA+ could convert to diagrams instead of Math notation.

Re: The Future of TLA+ [pdf]

#19

Post by klingoff » Wed, Aug 28, 2024, 8:49 PM UTC

Mathnerd314 wrote: post #9

> Simplicity is a major goal of TLA+. Is TLA+ simple? I find this hard to accept. > TLA+ isn’t a programming language; it’s mathematics. Mathematics is not executable, though, whereas TLA+ is. > TLA+ [is better] for its purpose than a programming language. "TLA+ is a formal specification language designed by Leslie Lamport for the specification of system behavior." "specification of system behavior" sounds like a pro…

> If there was a future, like a goal or a roadmap or something, it would be outlined

Where is the outline for English? French has a more structured oversight with organizations and goals, so it will beat English?

Re: The Future of TLA+ [pdf]

#20

Post by AlotOfReading » Wed, Aug 28, 2024, 8:49 PM UTC

colanderman wrote: post #11

Mathnerd314 wrote: post #9

> Simplicity is a major goal of TLA+. Is TLA+ simple? I find this hard to accept. > TLA+ isn’t a programming language; it’s mathematics. Mathematics is not executable, though, whereas TLA+ is. > TLA+ [is better] for its purpose than a programming language. "TLA+ is a formal specification language designed by Leslie Lamport for the specification of system behavior." "specification of system behavior" sounds like a pro…

TLA+ is only "executable" in the same sense that an algebraic expression is executable. It's perfectly possible to write things on TLA+ that can not be simply executed linearly. (These overlap to a great extent with the things which TLC rejects.) As a basic example, it's easy to write a statement with \A (unbounded universal quantification) whose truth can only be judged by a proof engine. Specification languages are…

Being able to create systems by writing specifications and having the computer figure out how to execute them was basically the point of fifth generation programming languages.

More relevant today, you can execute other "specification" languages like Coq and Idris because they support things outside the narrow feature set of specification usecases.

TLA+ isn't executable and doesn't look like an imperative language because the authors don't want it to be, not because there's some universal line dividing specification languages from programming languages. It's also one of the biggest hurdles to TLA+ usage.