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 reason for using TLA+ is that it isn’t a programming language; it’s mathematics.
I love TLA+, I’ve used it for a decade and reach for it often. I have a huge amount of respect for Leslie Lamport and Chris Newcombe. But I think they’re missing something major here. The sematics of TLA+ are, in my mind, a great set of choices for a whole wide range of systems work. The syntax, on the other hand, is fairly obscure and complex, and makes it harder to learn the language (and, in particular, translate other ways of expressing mathematics into TLA+).
I would love to see somebody who thinks deeply about PL syntax to make another language with the same semantics as TLA+, the same goals of looking like mathematics, but more familiar syntax. I don’t know what that would look like, but I’d love to see it.
It seems like with the right library (see my mathlib point) and syntax, writing a TLA+ program should be no harder than writing a P program for the same behavior, but that’s not where we are right now.
> The errors [types] catch are almost always quickly found by model checking.
This hasn’t been my experience, and in fact a lot of the TLA+ programs I see contain partial implementations of arbitrary type checkers. I don’t think TLA+ needs a type system like Coq’s or Lean’s or Haskell’s, but I do think that some level of type enforcement would help avoid whole classes of common specification bugs (or even auto-generation of a type checking specification, which may be the way to go).
> [A Coq-like type system] would put TLA+ beyond the ability of so many potential users that no proposal to add them should be taken seriously.
I do think this is right, though.
> This may turn out to be unnecessary if provers become smarter, which should be possible with the use of AI.
Almost definitely will. This just seems like a no-brainer to bet on at this stage. See AlphaProof, moogle.ai, and many other similar examples.
> A Unicode representation that can be automatically converted to the ascii version is the best alternative for now.
Yes, please! Lean has a unicode representation, along with a nice UI for adding the Unicode operators in VSCode, and it’s awesome. The ASCII encoding is still something I trip over in TLA+, even after a decade of using it.
I loved the concept of TLA+ and tried to get into it, but as you say
> The syntax, on the other hand, is fairly obscure and complex, and makes it harder to learn the language
the syntax was very non-standard which was off putting, and the expected dev ux seemed to be of the 'get it right on paper first then just write the text' variety. This was also off putting and I think you're right that there is a space for making a DX focused TLA+ transpiled language
> The [\EE] operator is needed to explain the theory underlying how
TLA+ is used.
There's another reason to potentially support \EE: it's needed to refine specs with auxiliary variables. Currently, if an abstract spec has `aux_hist` to prove a property or something, you need the refinement to have an `aux_hist` equivalent, even if it doesn't affect the spec behavior at all. But if checkers could handle `\EE` you could instead leave it out of the refinement and check `\EE aux_hist: Abstract(aux_hist)!Spec`.
I think /u/pron once told me that actually checking a property of that form is 2-EXPTIME complete, though. Which is why it's not supported in practice.
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]
> 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.
Yes, that's an interesting implementation. I'm using Firefox, and the jumps to the notes and back to the paragraph are recorded in history, and has the expected effect when clicking the back and forward history arrows/buttons.
As someone who's fascinated by formal verification and who's early in their career, what advice do senior folks who have been using TLA+ have?
TLA+ isn't taught in most universities and while I've read about so many interesting applications, I'm yet to convince myself that someone would hire me for knowing it rather than just teaching it to me on the job. Any tips to get started would also be appreciated!
There's very little tech that somebody is going to hire you for knowing. It's a tool like many others.
If nothing else, spending a few days playing with it will give you an idea of what it's good for and if you want to continue, or it'll make it stick in your mind so you can come back to it if you ever need it.
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.
I wouldn't say it's a TLA+ alternative because it cannot do the most powerful and useful things TLA+ does (esp. refinement), but it is an alternative for programmers who just want to specify at a level that closer to code and model-check specifications.
Whoa, I use TLA ironically to joke about Three Letter Acronyms, I had no idea that the Three Letter Acronym (TLA) was in any way related to Temporal Logic Actually. Fascinating!
TLA+ is 25 years old. Despite the power it's syntax is too alien to become mainstream.
Have you considered https://FizzBee.io?
Almost Python-like syntax, has more powerful semantics, beautiful visualizations with no extra work, only formal methods system that can do performance analysis.
> 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 programming language to me. A systems programming language, even.
All this is to say that it seems TLA+ really has no future. If there was a future, like a goal or a roadmap or something, it would be outlined in this document a lot more clearly - whereas, instead, it is more like "nope, everything's good, no changes needed", even as the language appears nowhere on the TIOBE rankings.
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.
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.
> "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.
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 rather than what defining the equivalent "programming function" in, say, Haskell would mean:
f :: Integer -> Integer
f x = -(f x)
> Mathematics is not executable, though, whereas TLA+ is.
It is definitely not executable (i.e. not any more than mathematics is; you can specify executable things in maths and therefore in TLA+, but not everything you specify is executable). You can specify non-computable things (e.g. it is trivial to specify a halting oracle) as well as things involving real numbers. Moreover, when you check a TLA+ specification with a model-checker like TLC, it doesn't actually execute the specification, as it can check a specification of uncountable many executions, each of infinite length in a second.
However, you can certainly write formulas specifying the behaviour of an executable program and simulate it with TLC. But this is because you can use mathematics to describe physical systems, but not everything you can describe in mathematics can have a physical representation.
> "specification of system behavior" sounds like a programming language to me. A systems programming language, even.
A program is, indeed, one way of specifying a system, and TLA+ does allow you to specify an algorithm in this way (because maths allows you to specify programs), but it also allows you to specify systems in very useful ways that are very much not programs. For example, you can specify a component that sorts things without ever writing an algorithm for sorting, which is useful when the details of the sorting algorithm are irrelevant to the questions you want to answer. It's like how you can write a formula that treats planets as point-masses if you're interested in orbital mechanics, yet specify the earth in a much more detailed way if you're interested in predicting the weather.
> even as the language appears nowhere on the TIOBE rankings.
It is not a programming language. While it is true that far more people write programs than use mathematics to reason about physics, biology, or the way software systems behave (especially complicated interactive and distributed systems, which is where TLA+ excels), that doesn't mean such disciplines have no future.
> 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.
mjb|1 year ago
> The reason for using TLA+ is that it isn’t a programming language; it’s mathematics.
I love TLA+, I’ve used it for a decade and reach for it often. I have a huge amount of respect for Leslie Lamport and Chris Newcombe. But I think they’re missing something major here. The sematics of TLA+ are, in my mind, a great set of choices for a whole wide range of systems work. The syntax, on the other hand, is fairly obscure and complex, and makes it harder to learn the language (and, in particular, translate other ways of expressing mathematics into TLA+).
I would love to see somebody who thinks deeply about PL syntax to make another language with the same semantics as TLA+, the same goals of looking like mathematics, but more familiar syntax. I don’t know what that would look like, but I’d love to see it.
It seems like with the right library (see my mathlib point) and syntax, writing a TLA+ program should be no harder than writing a P program for the same behavior, but that’s not where we are right now.
> The errors [types] catch are almost always quickly found by model checking.
This hasn’t been my experience, and in fact a lot of the TLA+ programs I see contain partial implementations of arbitrary type checkers. I don’t think TLA+ needs a type system like Coq’s or Lean’s or Haskell’s, but I do think that some level of type enforcement would help avoid whole classes of common specification bugs (or even auto-generation of a type checking specification, which may be the way to go).
> [A Coq-like type system] would put TLA+ beyond the ability of so many potential users that no proposal to add them should be taken seriously.
I do think this is right, though.
> This may turn out to be unnecessary if provers become smarter, which should be possible with the use of AI.
Almost definitely will. This just seems like a no-brainer to bet on at this stage. See AlphaProof, moogle.ai, and many other similar examples.
> A Unicode representation that can be automatically converted to the ascii version is the best alternative for now.
Yes, please! Lean has a unicode representation, along with a nice UI for adding the Unicode operators in VSCode, and it’s awesome. The ASCII encoding is still something I trip over in TLA+, even after a decade of using it.
vosper|1 year ago
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
pierrefermat1|1 year ago
Building out any real maths with logic operators yourself is just not feasible in a meaningful timescale.
vanjajaja1|1 year ago
> The syntax, on the other hand, is fairly obscure and complex, and makes it harder to learn the language
the syntax was very non-standard which was off putting, and the expected dev ux seemed to be of the 'get it right on paper first then just write the text' variety. This was also off putting and I think you're right that there is a space for making a DX focused TLA+ transpiled language
hwayne|1 year ago
There's another reason to potentially support \EE: it's needed to refine specs with auxiliary variables. Currently, if an abstract spec has `aux_hist` to prove a property or something, you need the refinement to have an `aux_hist` equivalent, even if it doesn't affect the spec behavior at all. But if checkers could handle `\EE` you could instead leave it out of the refinement and check `\EE aux_hist: Abstract(aux_hist)!Spec`.
I think /u/pron once told me that actually checking a property of that form is 2-EXPTIME complete, though. Which is why it's not supported in practice.
rtpg|1 year ago
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...
zozbot234|1 year ago
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.
bokumo|1 year ago
gurjeet|1 year ago
evomassiny|1 year ago
wizerno|1 year ago
TLA+ isn't taught in most universities and while I've read about so many interesting applications, I'm yet to convince myself that someone would hire me for knowing it rather than just teaching it to me on the job. Any tips to get started would also be appreciated!
kadoban|1 year ago
If nothing else, spending a few days playing with it will give you an idea of what it's good for and if you want to continue, or it'll make it stick in your mind so you can come back to it if you ever need it.
SonOfLilit|1 year ago
pnathan|1 year ago
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.
mjb|1 year ago
nektro|1 year ago
threatofrain|1 year ago
https://quint-lang.org/
pron|1 year ago
pnathan|1 year ago
lolinder|1 year ago
bvrmn|1 year ago
westurner|1 year ago
fat_cantor|1 year ago
jayaprabhakar|1 year ago
penguin_booze|1 year ago
I bet you a million dollars [0] that Mr. Lamport absolutely is the sole author of this sentence.
[0] which I don't have. You may resume reading.
leogss27|1 year ago
[deleted]
Mathnerd314|1 year ago
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 programming language to me. A systems programming language, even.
All this is to say that it seems TLA+ really has no future. If there was a future, like a goal or a roadmap or something, it would be outlined in this document a lot more clearly - whereas, instead, it is more like "nope, everything's good, no changes needed", even as the language appears nowhere on the TIOBE rankings.
Certhas|1 year ago
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.
colanderman|1 year ago
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.
tailrecursion|1 year ago
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.
pron|1 year ago
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:
What function is it? Clearly, it's the zero function rather than what defining the equivalent "programming function" in, say, Haskell would mean: > Mathematics is not executable, though, whereas TLA+ is.It is definitely not executable (i.e. not any more than mathematics is; you can specify executable things in maths and therefore in TLA+, but not everything you specify is executable). You can specify non-computable things (e.g. it is trivial to specify a halting oracle) as well as things involving real numbers. Moreover, when you check a TLA+ specification with a model-checker like TLC, it doesn't actually execute the specification, as it can check a specification of uncountable many executions, each of infinite length in a second.
However, you can certainly write formulas specifying the behaviour of an executable program and simulate it with TLC. But this is because you can use mathematics to describe physical systems, but not everything you can describe in mathematics can have a physical representation.
> "specification of system behavior" sounds like a programming language to me. A systems programming language, even.
A program is, indeed, one way of specifying a system, and TLA+ does allow you to specify an algorithm in this way (because maths allows you to specify programs), but it also allows you to specify systems in very useful ways that are very much not programs. For example, you can specify a component that sorts things without ever writing an algorithm for sorting, which is useful when the details of the sorting algorithm are irrelevant to the questions you want to answer. It's like how you can write a formula that treats planets as point-masses if you're interested in orbital mechanics, yet specify the earth in a much more detailed way if you're interested in predicting the weather.
> even as the language appears nowhere on the TIOBE rankings.
It is not a programming language. While it is true that far more people write programs than use mathematics to reason about physics, biology, or the way software systems behave (especially complicated interactive and distributed systems, which is where TLA+ excels), that doesn't mean such disciplines have no future.
foysavas|1 year ago
By "specification language" Lamport means one capable of verification via model checking.
In contrast, "programming languages" are not capable of such verification.
lolinder|1 year ago
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.
klingoff|1 year ago
Where is the outline for English? French has a more structured oversight with organizations and goals, so it will beat English?