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.
>There's very little tech that somebody is going to hire you for knowing. It's a tool like many others.
I guess this must be true on places like SF since I see this so often on HN, but almost every single job listing I've seen strictly requires knowledge of a specific tech stack, with the exception of a few internship programs.
There's tech that if it's not on your resume, you won't pass the first filter. But that's different. Knowing it will _not_ get you a job, it'll just get you past some early step.
But things like TLA+ are way different from even that. The number of programming jobs that will bin you if you don't have TLA+ on your resume has to be like, 5 in the world. Nobody is going to see it on there and be like "we _must_ hire this person!".
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.
P is very nice indeed, be advised that it is not an exhaustive checker like TLC (TLA+'s model checker, or Apalache, the symbolic tester). It is more like a higher-level testing framework.
That said, since non-deterministic choices are equi-probable in P, failure conditions are triggered at much higher frequencies than in a conventional testing scenario.
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.
Every time I see a new TLA+ replacement my first thought is "Oooh this will be good for the 99% of normal stuff people do with TLA+."
Then I look through some of the specs I've written with clients and find the one absolutely insane thing I did in TLA+ that would be impossible in that replacement.
I believe this is really the tragedy of formal verification tools. Everybody wants a tool as robust as a compiler. At the same time, nobody wants to invest into development of such tools. Microsoft Research 20 years ago was probably an exception to that. The other companies wish to immediately hide these tools and the benchmarks behind the IP and closed source. As a result, we have early stage MVPs that are developed by 1-3 people.
When you say peer reviews, do you mean academic publications or testimonials? I imagine it would be difficult to publish a paper at an academic conference proposing an alternative syntax for anything, even if it were better.
- 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 read the 2018 Transfomer paper "Attention is all you need".
They use human language, diagrams, and mathematics to describe their idea.
However if your try to build you own "Transformer" using that paper as your only resource your going to struggle interpreting what they are saying to get working code.
Even if you get the code working, how sure are you that what you have created is EXACTLY what the authors are talking about?
English is too verbose, diagrams are open to interpretation & mathematics is too ambiguous/abstract. And already written code is too dense.
TLA+ is a notation that tends to be used to "specify systems".
In TLA+ everything is a defined in terms of a state machine. Hardware, software algorithms, consensus algorithms (paxos, raft etc).
So why TLA+?
If something is "specified" in TLA+;
- You know exactly what it is — just by interpreting the TLA+ spec
- If you have an idea to communicate. TLA+ literate people can understand exactly what your talking about.
- You can find bugs in an algorithms, hardware, proceseses just by modeling them in TLA+.
So before building Hardware or software you can check it's validity & fix flaws in its design before committing expensive resources only to subsequently find issues in production.
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?
It’s really not, TLA+ works best for modeling state machines with few discrete states and concurrent systems. It can find interesting interleaving of events that would leave to a violation of your system properties
> What Formal Specification Is Not Good For: We are concerned with two major classes of problems with large distributed systems: 1) bugs and operator errors that cause a departure from the logical intent of the system, and 2) surprising ‘sustained emergent performance degradation’ of complex systems that inevitably contain feedback loops. We know how to use formal specification to find the first class of problems. However, problems in the second category can cripple a system even though no logic bug is involved. A common example is when a momentary slowdown in a server (perhaps due to Java garbage collection) causes timeouts to be breached on clients, which causes the clients to retry requests, which adds more load to the server, which causes further slowdown. In such scenarios the system will eventually make progress; it is not stuck in a logical deadlock, livelock, or other cycle. But from the customer's perspective it is effectively unavailable due to sustained unacceptable response times. TLA+ could be used to specify an upper bound on response time, as a real-time safety property. However, our systems are built on infrastructure (disks, operating systems, network) that do not support hard real-time scheduling or guarantees, so real-time safety properties would not be realistic. We build soft real-time systems in which very short periods of slow responses are not considered errors. However, prolonged severe slowdowns are considered errors. We don’t yet know of a feasible way to model a real system that would enable tools to predict such emergent behavior. We use other techniques to mitigate those risks.
Formal methods including TLA+ also can't/don't prevent or can only workaround side channels in hardware and firmware that is not verified. But that's a different layer.
> This raised a challenge; how to convey the purpose and benefits of formal
methods to an audience of software engineers? Engineers think in terms of debugging rather than ‘verification’, so we called the presentation “Debugging Designs” [8]
. Continuing that metaphor, we have
found that software engineers more readily grasp the concept and practical value of TLA+ if we dub it:
Exhaustively testable pseudo-code
> We initially avoid the words ‘formal’, ‘verification’, and ‘proof’, due to the widespread view that formal
methods are impractical. We also initially avoid mentioning what the acronym ‘TLA’ stands for, as doing
so would give an incorrect impression of complexity.
Isn't there a hello world with vector clocks tutorial? A simple, formally-verified hello world kernel module with each of the potential methods would be demonstrative, but then don't you need to model the kernel with abstract distributed concurrency primitives too?
Formal specifications benefits are clear and I think well understood at that point. If you want to ensure that your specifications is coherent and doesn’t have unexpected behaviour, having a formal specification is a must. It’s even a legal requirement for some system nowadays in safety critical applications.
The issue of TLA+ is that it doesn’t come from the right side of the field. Most formal specifications tools were born out of necessity from the engineering fields requiring them. TLA+ is a computer science tool. It sometimes shows in the vocabulary used and in the way it is structured.
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.
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.
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.
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.
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.
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.
> 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're not the same thing.
> 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.
Coq and Idris are very different in the way they're typically used, and I'd say TLA+ is much closer to Coq than to Idris (and is probably more popular than the two combined), but to "execute" anything the specification needs to be at a certain level that's detailed enough to produce a program, and oftentimes that is very much not what you want.
It would be extremely useful to have a language that you could describe the various properties of a car and it would compile your specification into the design of a car (you would need to give it sufficient detail as there are choices to be made). But it would also be extremely useful to have a language that could be used to learn certain things about a car -- say, it's braking distance -- without specifying it in sufficient detail to actually build one. That is what maths is good for -- describing things at arbitrary levels of detail to answer relevant questions.
For example, you may have a 5 MLOC distributed system, and you want to know if a certain kind of failure may lead to data loss. You could use TLA+ to describe just the relevant details to answer the question in, say, 200 lines of formulas. That you cannot compile those formulas into a working 5 MLOC piece of software is not a downside of mathematics, but rather the point.
> TLA+ isn't executable and doesn't look like an imperative language because the authors don't want it to be
And because it's not a language for programming but a language for mathematics, so it looks and feels pretty close to plain mathematics (only it's formal), as that's the obvious choice for writing mathematics.
> 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.
I don't understand the order of your implication. You can use maths (say, some ZFC formalism) to specify the execution of any Python or Java or C program and even write a software tool that executes it. It's the converse that isn't true: You cannot write a Python or Java or C program that accurately expresses many mathematical theorems (e.g. you can only express computable numbers in a program). I.e. the expressivity of mathematics includes that of programming, but not vice versa.
In TLA+ you can express every theorem in ZFC, but that doesn't mean you can automatically prove or disprove every proposition or even every theorem, because that is indeed a limitation of mathematics. There are also lots and lots of theorems you can state and prove in TLA+ yet not prove automatically with the TLC model-checker (or, indeed, with any known automatic proof method). That is a limitation of TLC (or of any known automatic proof methods), but not one of TLA+.
Coq, specifically Gallina, is absolutely a specification tool. It's not only that, but it's one of the big use cases it's explicitly designed to support.
No, it’s not. Gallina is not a specification tool in the way TLA+ is (even if coq calls it its specification language). Gallina is a language used to write mathematical statements which you intend to prove. It’s not designed to write specifications.
Coq is definitely not a specification tool. You can probably prove a specification with it in the same way you actually can do symbolic manipulation with C if you really want to. It still remains an interactive prover.
> "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.
> 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)?
* 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.
f ≜ CHOOSE f ∈ [Int → Int] :
∀ x ∈ Int : f[x] = -f[x]
You added the > in your quote of pron, he didn't have it in the original. There is no c in ℤ with c != 0 s.t. f(x) = c and f(x) = -f(x), that would imply that c = -c for non-zero integers which is not true. The only function that can satisfy pron's constraints is f(x) = 0 since c = 0 is the only time
c = -c, or 0 = -0.
Ah yes "f triangle equals CHOOSE f member of array of int to int, namely, upside down A x member of int, namely, x'th element of f equals the negative of x'th element of f." Easier than python indeed, where this simple and elegant expression is turned into the much more complicated and ugly form of
f == CHOOSE f \in [Int \X Int -> Int]:
\A <<x, y>> \in DOMAIN f:
f[x, y] = f[y, x]
Which is expressing that `f` is some commutative function, but we don't care which. Could be multiplication, could be addition, could be average, could be euclidian distance from origin, could just be the 0 function.
You could say you ignored math classes in a more short form. Parent describes a selection of element (f) from a set of functions such that `f(x)` equals `-f(x)`. Your python example is quite far from that.
If a projects desires a future, it requires adoption. For that, it must be approachable. When the syntax throws unicode math symbols at the user, and requires the user to first define the universe before even thinking about "this function negates the input", and in general throws years of programming language syntax conventions away, it's just not approachable.
I understand and empathize with the ideal that everyone should just know college level math. It may even be fun to engage in putting down those who don't. Oh, how they just ignored their classes! Stupid fools!
However, it's not a realistic expectation, even in the field of programming, where a large majority have not been accredited with a math bachelors degree. A LOT of programmers didn't even have computer science formal education.
Meet people where they are and all that. Taking position in an ivory tower allows you to feel intellectually superior, but practically speaking it doesn't actually get you anywhere.
The TLA+ community can not have it both ways, either stop bemoaning the lack of adoption of formal verification, or adapt to meet people where they are at. And certainly don't make redditor-esque proclamations about "just" "simply". Take a step back and think about your goals when you write in such a tone. Are you trying to build something and invite others? Or are you trying to prove your own intellect? To whom and what for?
Man. I completely understand your frustration. It's similar how music-illiterate people whine about standard music notation. The math notation in question is literally 30min intro to a set theory. There is no knowledge gate and towers to conquer. Been there and the real ultimate answer: it's a matter of spending a little time and learn stuff.
> If a projects desires a future, it requires adoption. For that, it must be approachable.
But TLA+'s past, present, and future, is as a language for writing mathematical specifications. When you compare it to other languages for writing mathematics, like Coq or Lean, you will see that it is, indeed, much more approachable and orders of magnitude easier to learn. Writing mathematics in Python syntax is not only foreign but also quite inapproachable and confusing, because the meaning of things like functions and operators are so different in Python and mathematics. Using the same syntax for things that work very differently is not helpful.[1]
Now, TLA+ is not a programming language, it's not trying to compete with programming language, and like mathematics in general, it can never hope to have as many practitioners as there are programmers. It is, however, already the most popular language for writing mathematical specification of software and hardware, because programmers and hardware designers can learn and apply it much quicker than they can Lean or Coq.
Not every programmer is interested in using mathematics to specify digital systems, but some fund it very useful, and for some it's even necessary.
> The TLA+ community can not have it both ways, either stop bemoaning the lack of adoption of formal verification, or adapt to meet people where they are at.
You do have a point, but it's complicated. Mathematics is inherently more expressive than programming, and so there are often specifications that are simply much easier to write in maths than in a programming language. Writing maths in programming-language syntax is not helpful and is even a hindrance, and the problem is that it's not that a lot of programmers don't want to learn mathematical syntax; they just don't want to learn that discipline. and that's fine; I'm not currently interested in learning Japanese, but it's not because written Japanese uses symbols that are unfamiliar to me. Even if I could learn Japanese using the Latin alphabet, I'm not sure it would make things significantly easier; at best it would make things slightly easier at the cost of me not being able to employ Japanese as much in practice.
So formal methods have a choice between specifying with programming language -- which makes the method more easily adoptable by programmers but makes some very useful specifications impossible -- or use mathematics to allow people to write simpler, shorter, and more powerful specifications, but require them to learn the basics of specifying with mathematics.
What do we do? Both! There are specification languages that aim to be programming languages (or similar to programming, and somebody here mentioned Quint, which is one of the languages that do just that), and there are specification languages that are simpler and more powerful, but they are very much not programming and they don't resemble programming, and TLA+ is a language like that.
> Are you trying to build something and invite others?
Yes.
> Or are you trying to prove your own intellect?
People speaking German aren't trying to prove their intellect, it's just that I have never learnt it. There is no more intellect in using basic mathematics to specify things than in programming. If anything, I think programming is much more difficult (of course it's more common, largely due to economic incentives). But the disciplines are different. There is no more intellect in writing newspaper columns than in writing Python programs, but they are not the same, and if you want to do both you'd need to learn both.
> To whom and what for?
To those who are interested in the most powerful way to reason about the behaviour of engineered systems and are willing to spend a couple of weeks learning something that is very much outside the discipline of programming to do so. Having a tool that allows you to do that is important. I learnt TLA+ over 10 years ago when I was designing a protocol for a distributed system and ran into some subtle and dangerous bugs. TLA+ was then, and is now, the tool that most cheaply and easily allowed me to find the flaw in my algorithm and verify that an improved algorithm doesn't suffer from it. If you're using AWS directly or indirectly, you are using software that was designed with the help of TLA+.
TLA+ is not for every programmer simply because not every programmer writes software that TLA+ is the best tool to assist with, but I think that more people could find TLA+ helpful than they realise. But TLA+ is so helpful in those cases because it can be much more expressive than anything that could be expressed in a programming language.
Others may certainly find more programming-like specification languages more useful, and that's great, too! The more people know how to use various formal methods and when each may be more or less applicable, the better software will become.
[1]: Here's an example where TLA+ syntax is similar to programming:
A(x, y) ≜ x + y
This defines an operator A(x, y), that is equal to x + y. This looks similar enough to defining a subroutine in a programming language, but thinking about it that way will be confusing if you see seomthing like:
A(x, y)' = 3
which means "the sum of x and y will be 3 at a future instant". The more correct way of thinking about the definition of the operator is that its definition may be substituted in any occurrence of the operator (i.e. you can write `x + y` whenever you see A(x, y)). This isn't like a subroutine even in a language like Haskell. Also, it's not a cute idiosyncrasy, but actually important when you want to express the similarities between two different specifications (often at two different levels of detail), something that is very useful.
it would have, indeed, been an identical definition -- the value of f(x) is equal to -f(x) -- but it's meaning is completely different from the one in TLA+ (and mathematics). Unlike the TLA+ function, the Python function is not zero for all integers. That was my point: TLA+ isn't and doesn't behave like programming; it's mathematics.
Second, on the question of simplicity. Let's talk semantics first. If I tell you you have a function f(x) on the integers such that f(x) = -f(x), it's quite simple to understand that the function is zero everywhere. Yet, it's not the case in Python (or C or Java or Haskell) because what they do is far more complicated. To understand why it's not zero, you have to know a lot more. The behaviour of that definition in Python is a lot more complicated than the behaviour of the function in TLA+, it's just that since you've already spent a significant amount of time learning the fundamentals of programming and computers, you already know that complicated stuff, so there isn't much for you to learn. But if you don't already know programming, then learning the basic mathematics of TLA+ and how they work would be easier than learning the basics of programming and how computers work so that you'd understand why f(x) in Python is not the zero function. How helpful would it be to use Python syntax if the meaning of how functions work would be completely different from Python's?
Let's take a look at another simple example:
Inc(x) ≜ x + 1
You may think it works like:
def Inc(x):
return x + 1
but it doesn't, because (assuming you specify that x is always an integer, a detail I'll skip for the sake of this example), you need to be able to write things like:
3 = Inc(x)'
Because it's maths, we can substitute:
3 = (x + 1)'
Then apply the rules of the prime operator:
3 = x' + 1
Subtract 1 from both sides, as that preserves equality:
2 = x'
Equality is symmetric:
x' = 2
And so 3 = Inc(x)' specifies the same as assigning 2 to be the next value of x, because in maths you can manipulate expressions by substitution and application of very simple rules. Writing it in this way can be very important and extremely useful when reasoning about the similarity of two different specifications of the same algorithm.
That's how maths (and so TLA+) works, but it's not how programming works, and thinking of operator or function definitions as if they were like subroutine definitions only serves to confuse.
This brings us to the matter of syntax. TLA+ is a language for writing mathematics, and it uses a syntax that is quite similar to standard mathematical notation (certainly more similar than Python is to standard notation) as it's been in use for over 100 years. When you write mathematics, that is the syntax you'd expect. TLA+ differs from standard notation in some interesting ways because much thought has gone into designing the syntax to serve a purpose (e.g. https://lamport.azurewebsites.net/pubs/lamport-howtowrite.pd...), but that purpose is very much not programming, but reasoning about programs. This is as it works in other engineering disciplines, too: a sophisticated CAD/CAM tool may be used to help construct something, but ordinary mathematics is used to reason about certain important aspects of the thing.
Standard notation is not always consistent, but it does have qualities that are desirable when writing mathematics, especially when it comes to substitution. In TLA+, as in mathematics, writing x = 3 means the same as writing 3 = x. It's both strange and complicates matters considerably that in Python this is not the case (indeed, in programming you cannot substitute things as freely as in maths/TLA+).
In this case, too, the Python syntax seems simpler to you because you already know programming and maybe you're less familiar with standard mathematical notation (it would take you no more than a few hours to learn it), but if you tried writing maths in Python, you'd find that the syntax is not simple at all. That is because Python is a language for writing programs and the syntax is optimised for that purpose. TLA+ is a language for writing mathematics, and the syntax is optimised for that purpose. But mathematics is simpler than Python programming which you can see both in how complex it is to fully specify (ZFC vs Python that is) and also in how much easier it is to learn (assuming, of course, you don't already know most of what it is that you're supposed to learn).
> 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.
Also, being popular is not the same as being useful. Mathematica and Verilog aren't on the TIOBE either, and Verilog is a lot more important to society than Logo!
> 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.