Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The Future of TLA+ [pdf]

lamport.azurewebsites.net

Post reply on HN
Print view View original

41–50 of 107 posts

Re: The Future of TLA+ [pdf]

#41

Post by rtpg »

I'm really not a fan of TLA+'s tooling, but I do really love the temporal logic. I've always kinda wanted that stuff in other proving languages, but I don't know how possible it is.

Would it be actually possible to write something like an "a la carte temporal logic library" for other proving languages that could get you some of the confidence you can get from TLA+'s modeling?

(Aside: I have a TLA+ book, but it's notably missing really much in terms of exercises or anything. If anyone has any recommendations for a large set of exercises to play around in the space I'd love to hear about it!)

EDIT: turns out just searching for "temporal logic in X language" gets you papers, found this one paper for axiomatizing temporal logic that seems to be a good starting point for anyone looking at this [0]

[0]: https://lim.univ-reunion.fr/staff/fred/Enseignement/Verif-M2...

Re: The Future of TLA+ [pdf]

#42

Post by zozbot234 »

rtpg wrote: post #41

I'm really not a fan of TLA+'s tooling, but I do really love the temporal logic. I've always kinda wanted that stuff in other proving languages, but I don't know how possible it is. Would it be actually possible to write something like an "a la carte temporal logic library" for other proving languages that could get you some of the confidence you can get from TLA+'s modeling? (Aside: I have a TLA+ book, but it's nota…

> Would it be actually possible to write something like an "a la carte temporal logic library" for other proving languages that could get you some of the confidence you can get from TLA+'s modeling?

Temporal logic is just a specific instance of a modal logic, which can be modeled with reasonable ease using a "possible worlds"-based encoding. Note that TLA+ combines temporal logic with non-determinism, which is a different modality.

Re: The Future of TLA+ [pdf]

#43

Post by Mathnerd314 »

pron wrote: post #36
AlotOfReading wrote: post #20

Earlier quoted context omitted.

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 be…

> 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. Yeah, but in maths you can specify anything, including things that the computer is unlikely to figure out how to execute if it's possible at all. Programming languages of every generation are very useful, as is mathematics, even though they'…

> in maths you can specify anything, including things that the computer is unlikely to figure out how to execute if it's possible at all.

Well, in TLA+ you can write programs that run forever (or at longer than you'll live) and don't do anything like "model check" or whatever you want to call executing TLA+, even though they are perfectly sound mathematically. This should make it clear that TLA+ is not maths.

Re: The Future of TLA+ [pdf]

#44

Post by vosper »

mjb wrote: post #38

I may have been spending too much time with Lean recently, but the number one thing I’d like to see for the future of TLA+ is an equivalent of Mathlib ( https://github.com/leanprover-community/mathlib4 ). What’s so great about the experience of using Lean is that I can pull theorems off the shelf from Mathlib, use them if I want to, or learn from the way their proofs work if I want to do something similar. > The reas…

> I would love to see somebody who thinks deeply about PL syntax to make another language with the same semantics as TLA+

Perhaps you would find Quint interesting? https://news.ycombinator.com/item?id=41111790

There's a comment that says Quint uses TLA+ as its base language: https://news.ycombinator.com/item?id=41118162

Disclaimer: I don't know anything about TLA+ or Quint, I just remembered seeing Quint here

Re: The Future of TLA+ [pdf]

#45

Post by Mathnerd314 »

Certhas wrote: post #13
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 syst…

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.

Re: The Future of TLA+ [pdf]

#46

Post by pnathan »

I was looking at TLA a few months ago to consider what it would take to prove multiregion fail over worked correctly. Considering I'd never looked at it before.

I did not find it straight forwardly grokkable, which makes me sad. Maybe it needs a library of axioms? I feel there's probably a very nice way to work through it without ingesting effectively a graduate school course in proving software.

It really is just math and proofs, it shouldn't be so hard... to start.

Well, that's my take. Could be wrong. Might just need to hit the books.

Re: The Future of TLA+ [pdf]

#48

Post by erichocean »

Mathnerd314 wrote: post #45
Certhas wrote: post #13

Earlier quoted context omitted.

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 syst…

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 ge…

> Math is a natural language

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

Re: The Future of TLA+ [pdf]

#49

Post by zekrioca »

pron wrote: post #31
zekrioca wrote: post #28

Earlier quoted context omitted.

> It is very, very simple, and I would say easier to learn than Python, as long as you remember that it is not programming but maths. For example, suppose you specify this function on the integers: > f ≜ CHOOSE f ∈ [Int → Int] : > ∀ x ∈ Int : f[x] = -f[x] > What function is it? Clearly, it's the zero function Did you mean your example is the constant function [1], rather than a zero function [2] (where c = 0)? [1] ht…

I mean the zero function, i.e., the one that is zero everywhere, because if y ∈ ℤ and y = -y, then y = 0.

Doesn't ℤ include negative natural numbers?

* Nevermind, I just saw you used the ">" sign in the definition. Is it why the definition only applies to positive numbers? In any case, you did not write it in your textual description, which looked confusing to me. I think it would be easier if one could define it as ℤ+ or something like that.

Re: The Future of TLA+ [pdf]

#50

Post by pierrefermat1 »

mjb wrote: post #38

I may have been spending too much time with Lean recently, but the number one thing I’d like to see for the future of TLA+ is an equivalent of Mathlib ( https://github.com/leanprover-community/mathlib4 ). What’s so great about the experience of using Lean is that I can pull theorems off the shelf from Mathlib, use them if I want to, or learn from the way their proofs work if I want to do something similar. > The reas…

I've only play with TLA+ for a small amount of time but absolutely agree with the maths statement being way off the mark.

Building out any real maths with logic operators yourself is just not feasible in a meaningful timescale.

Post reply on HN