The Future of TLA+ [pdf]
lamport.azurewebsites.net
lamport.azurewebsites.net
> 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.
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
Building out any real maths with logic operators yourself is just not feasible in a meaningful timescale.
> 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
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.
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...
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.
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!
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 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.
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 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.
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.
- 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 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.
> 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.
Delay, cycles, feedback; [complex] [adaptive] nonlinearity
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
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?
From https://news.ycombinator.com/item?id=40980370 ;
> - [ ] DOC: learnxinyminutes for tlaplus
> TLAplus: https://en.wikipedia.org/wiki/TLA%2B
> awesome-tlaplus > Books, (University) courses teaching (with) TLA+: https://github.com/tlaplus/awesome-tlaplus#books
FizzBee, Nagini, deal-solver, z3, dafny; https://news.ycombinator.com/item?id=39904256#39938759 ,
"Industry forms consortium to drive adoption of Rust in safety-critical systems" (2024) https://news.ycombinator.com/item?id=40680722
awesome-safety-critical:
I wonder if TLA+ could convert to diagrams instead of Math notation.
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.
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.
Shoutout to operator labels.
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.
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.
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.
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.
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.
The fact that you can formalise a specification in order to prove it doesn't make Coq a specification tool.
I don't think software that needs specs should be done by people without a PhD. Jokes aside, I am not saying that Coq is an easy or simple specification tool. But of course it is a specification tool. Actually, it is one of the very few serious specification tools out there.
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.
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.
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+.
Now regarding TLA+ vs TLC, I am not clear what the utility of a TLA+ program that cannot be checked with TLC / TLAPS / etc. When you say "prove" a TLA+ program I first thought this was formally checking it with TLC / TLAPS / etc. But it seems you have a different notion of proof, some sort of handwaving "it looks right" notion. From my perspective this reduces a TLA+ program to a piece of writing, since nothing automated can be done with it. You might as well say "You can express every theorem in ZFC in Java by writing it in a comment" - it is not an informative observation. The interesting TLA+ programs are the ones that can be checked with TLC / TLAPS / etc., and to the extent one can work with these programs programmatically, TLA+ is a programming language.
But TLA+ formulas not programs for a proof checker. There is a model checker than can check some subset of TLA+ and a proof checker that can check some TLA+ proofs (if they're detailed enough to be checked), but you can even write proofs in TLA+ that TLAPS cannot check.
> Now regarding TLA+ vs TLC, I am not clear what the utility of a TLA+ program that cannot be checked with TLC / TLAPS / etc.
First, there is no such thing as a TLA+ "program". You write mathematical definition and state propositions. Second, that's like saying that it's not clear what the utility of any formal mathematics without tools, but formalisms were invented long before there were computers.
You can prove things without having them checked by a proof checker -- indeed that is how nearly all mathematical theorems have been proven -- and it's a rigorous process that isn't at all the same as things just "seeming" right.
Obviously, most of the practical usage of TLA+ involves use of TLC, some smaller amount involves the use of TLAPS, but whether or not you think there is utility in mathematics without mechanised tools, it doesn't change the fact that TLA+ is formalised mathematics.
> From my perspective this reduces a TLA+ program to a piece of writing, since nothing automated can be done with it.
It's not a program, and often times mathematics is "a piece of writing that nothing automated can be done with."
> The interesting TLA+ programs
Not programs, formulas. Again, they cannot be executed, although their veracity could be checked. Here is a TLA+ specification: `3 * 3 = 9`. Here is another one: `∀ x ∈ Nat : x * x ≥ x` [1]. These two can easily be checked to be true, yet they are not programs. Sure, mathematics can (and is) used to describe aspects of the dynamics of a thrown ball or of an algorithm, but that doesn't make mathematics a ball-manufacturing machine nor a programming language. You can use TLA+ to specify the quicksort algorithm and prove that it, indeed, sorts its input, but you don't use it to produce an executable program that sorts a list (unless you use a very limited subset and write a tool that can translate formulas of certain forms to a computer program).
[1]: I'm eliding some details because TLA+ formulas are interpreted in the TLA logic, where formulas have very specific semantics, but it's close enough for our purpose.
It is a program when I can do java tlatk.TLC someprogram.tla.
You say `3 * 3 = 9` is a TLA+ specification. Well, here is a Prolog program: 3*3 #= 9. Is there a difference? No. The output when I run the Prolog program? "yes". The output when I run the TLC program? I haven't tried, but it is probably similar to "yes" or "no". It is in this sense that you can run TLA+ programs and get a relatively small output of whether it checks. Maybe you don't consider this programming, but people have done more with less, e.g. lambda tarpits where all that happens is lambdas reduce to more lambdas. In contrast the value space of TLA+ is quite rich, it is only the usability of it that is limited because Leslie Lamport continues to insist that TLA+ is "not a programming language".
TLC is a program that takes TLA+ formulas as input and produces an output. I have a program that reads newspaper articles out loud. Doesn't make those articles programs or their authors programmers.
> Is there a difference? No
You're using implication in the wrong direction. Some mathematics can indeed appear in a programming language, but the question is not whether there's something in TLA+ that could be in Python or whether you can specify a Java program in TLA+ -- of course you can. The question is whether there's something in TLA+ that cannot be in a programming language, and, indeed, there is. All Prolog programs are programs; you can run them. Not only can you not many TLA+ specifications (or mathematical formulas in general) in a similar way to a program, many mathematical formulas cannot possibly describe any program that's implementable in the real world. You can write mathematical propositions about non-computable real numbers; you can specify a decision oracle for the halting problem (and because you can do it in mathematics, you can write it formally in TLA+).
Similarly, the fact you can specify orbital dynamics in maths doesn't make it physics, and it's easy to see it's not physics because you can just as easily specify motion that breaks physical laws.
> Maybe you don't consider this programming, but people have done more with less
You can certainly run computer programs that tell you interesting stuff about a TLA+ specification, and you can even say that the existence of such programs is the source of much of the value in TLA+. But you can run interesting and useful programs that do stuff with images, yet however you want to look at it philosophically, most photographers and programmers would agree that photography and programming are two pretty different disciplines even though photographers may use software in their work.
There's another interesting distinction to be made between Idris, a programming language that can also express a lot of maths, and TLA+, a mathemtatical language that isn't a programming language.
Languages like Idris make a sharp distinction between the type level and the object or computation level. The type level can express something analogous to the propositions you can express with TLA+, but these propositions must be filled or "realised" with content at the object level, and that content is required, even at the syntax level, to be a program, i.e. something that is executable.
In TLA+, in contrast, there's only a "type level". You can define refinement relationships between different specifications -- i.e. one is a more detailed description of the other -- but there is no requirement that any level needs to be executable. It may just so happen that some specification are detailed enough to extract a computation from (same goes for mathematics in general), but that's not a requirement.
BTW, it is interesting to note (as I do here in more detail: https://pron.github.io/posts/tlaplus_part3#algorithms-and-pr...) that quite often even simple algorithms -- I give QuickSort as an example -- that are described in a way that's detailed enough for a human to implement and perhaps even a computer could extract a reasonable computation from, are still not a program. The QuickSort algorithm says nothing about how to pick a pivot because any choice would still be an implementation of QS, even though a program must pick a pivot somehow and some choices may be better than others, nor does it describe in what order to sort the two segments -- they could be sorted in any order or even in parallel. For there to be a program, the computer must ultimately be told these details. Still, the algorithm is specified without them, as they don't matter to the algorithm itself, and it can be formally specified in TLA+ without them. If you choose, you may specify a particular and less abstract implementation of QS in TLA+ and check that it is, indeed, an implementation of the more abstract algorithm.
This could be seen as analogous to the object level in a programming language with dependent types, but the difference is that in TLA+ it's not required nor is there a clear distinction between a level of detail that is executable and one that isn't.
Main == PrintT("hello world")
You can't write much else, because print is the only implemented command (no input commands even), but it's clearly not just a program that reads newspapers out loud. There is an execution semantics and so on, as found in typical programming languages. It would not be hard to add input, implemented as a "hack" along the lines of print, although of course TLA+ is nondeterministic like most logic programming languages so there is some tricky semantics.
I'm not saying TLA+ is a good programming language - it is more along the lines of Brainfuck or TeX, "use it only out of necessity or masochism". But at least in my book it is undeniably in the category of programming languages.
That's not a good example, but before I get to that, you are again using logical implications in the wrong direction. You can describe physical systems, including programs in mathematics. What makes mathematics not the same as physics or programming is that you can also describe things that aren't physical or computable. It's like you're trying to prove that New York is the United States by pointing out that if you're in NY you're in the US.
Let me write that another way: programming ⊊ mathematics.
So you can write all programs in mathematics; you cannot do all mathematics in a programming language. Therefore, to know whether TLA+ is programming or mathematics the question is not whether you can describe programs in TLA+ but whether you can describe the maths that isn't programs, and you can.
Now, the reason that your example is not good is that the PrintT operator is defined in TLA+ [1] like so:
PrintT(x) ≜ TRUE
You could, however, have pointed out that you can specify a Hello, World program in TLA+, only that is unsurprising because you'd specify it in mathematics, and mathematics can also specify a Hello, World program. Here's how I would specify such a program in TLA+ (ignoring liveness for the sake of simplifying things):
VARIABLE console
Spec ≜ console = "" ∧ □[console' = "Hello, World!"]_console
You could also specify it another way, say, represent the console as a function of time (I'll make it discrete for simplicity):
console[t ∈ Nat] ≜ IF t = 0 THEN "" ELSE "Hello, World!"
[2]: I've even given a talk about such tricks: https://youtu.be/TP3SY0EUV2A
No, it is defined like so: https://github.com/tlaplus/tlaplus/blob/0dbe98d51d6f05c35630... This is the same strategy that Haskell uses for its primops, a placeholder file and implementation in another language. I guess you didn't understand my point that it would be easy to extend TLA+/TLC to more primops, like memory, a Java FFI, and so on, making it a fully featured programming language. I don't care what "the TLA+ language" is, C++ implementers regularly toss the spec in the dumpster and just like you have C++/LLVM and C++/GCC there similarly is a dialect of TLA+ for each implementation.
No, you are looking at the TLC source code, not TLA+ definitions. If you read the TLC documentation, it makes it very clear that it is not TLA+, but a software tool for model checking a certain subset of TLA+ and has some programming-like features that are not in TLA+. Other TLA+ tools also focus on other TLA+ subsets and have their own features, and they're not necessarily consistent with one another.
> This is the same strategy that Haskell uses for its primops
It really isn't, because TLC isn't the TLA+ compiler/interpreter. In TLA+ PrintT is just synonym for TRUE. We can talk about TLC if you like, but you shouldn't confuse the two.
> I guess you didn't understand my point that it would be easy to extend TLA+/TLC to more primops
TLA+ and TLC are two different things. TLA+ is a formal language for writing mathematical specifications. TLC is one of the several tools for analysing TLA+ specifications written in a subset of TLA+.
> I don't care what "the TLA+ language" is
That would sort-of made sense if TLC was the canonical tool for analysing TLA+ but it isn't (certainly not in the sense that ghc is the canonical Haskell compiler). In SANY, TLAPS, and Apalache (another TLA+ model checker), PrintT is just TRUE. In our work on the TLA+ toolbox, we're always careful to separate what's TLA+ and what are the features of the software tools, and in the materials we produce about TLA+ and the TLA+ tools these differences are explained.
In other words, you -- as someone who doesn't know TLA+ -- may not care about what TLA+ is and what TLC is, but those who use TLA+ very much care (though maybe not in the first week), because that distinction is required to put the language to good use.
If you choose to learn TLA+, I'm confident you'll come to agree. Everything I've said here will become clear once learn TLA+, TLC, and TLAPS (or even just TLA+). Those who actually use TLA+ very much do care what "the TLA+ language" is and what are some TLC features, because they often want to use multiple tools to do different things with their specifications, and PrintT only prints stuff when you're using TLC, not, say, when you're using TLAPS or Apalache. Once you gain experience with TLA+ you understand which subset of it can be checked by TLC and which isn't, and you write certain specifications with the intent of checking them in TLC and others for other uses, as you know that they fall outside TLC's subset of TLA+.
I think this short talk I gave and I linked to before (https://www.youtube.com/watch?v=TP3SY0EUV2A) gives a sense of the different ways you use TLA+ and how you combine them. It shows how you use the language as you do ordinary maths -- by manipulating formulas on paper -- and then use the results in conjunction with TLC to obtain some particular kind of automation. In fact, it is about how to use TLA+ to rewrite some TLA+ specifications so that they could be checked in some interesting way by TLC, i.e. the whole premise is that TLA+ users are confronted by the differences between TLC and TLA+, and it shows how to use certain deductions in practice to put TLC into some interesting uses for kinds of TLA+ specifications that TLA+ users would normally think fall outside the bounds of TLC. Anyway, anyone who actually uses TLA+ is -- and needs to be -- very much aware of the differences between TLA+ and TLC, recognises their different roles.
Fine, clearly you are missing the point I am making about how languages become confused with implementations. Just s/TLA+/TLC/ in all the above. Is TLC a programming language implementation or not? Consider for example https://github.com/will62794/tlaplus_repl which evaluates TLC expressions. At what point is there sufficient programming language functionality for you to become convinced that TLC is a programming language?
> Is TLC a programming language implementation or not?
Ok, so first of all, TLC is not "an implementation of TLA+" and not because it can only check a limited subset of TLA+.
To sho that, let me take a short but important detour. What is the purpose of a computer program? It is to produce an output, either for yourself or for others you give the program to. In contrast, what is the purpose of a TLA+ specification, i.e. what is it that you do with it, or what is the deliverable? Clearly, it's not some output because a TLA+ specification has no output (I'll get back to TLC in a moment). Once you're convinced that the TLA+ specification fulfils the propositions you're interested in -- either by inspection, formal manipulation and proof on paper, formal proof checked by TLAPS, or a successful run of TLC -- the deliverable is the TLA+ specification itself, the set of formulas, whose purpose is then for someone (maybe yourself or someone else) to use as a design for some system to build -- a program, a computer chip etc.. So a the purpose and deliverable of a TLA+ specification is it itself, just like the purpose of an architectural blueprint.
Now, back to TLC. TLC is, no doubt, a program that takes as an input a TLA+ specification written in a particular subset of TLA+ and some additional configuration that defines the boundaries of state space to model-check, and produces an output that's either TRUE or a counterexample. There are other modes of running TLC, as well, for which special operators like PrintT can be useful.
Note that there are many other programs that do something with a piece of mathematics and produce an answer. The simplest one is a calculator. A calculator is a program that takes as an input some portion of a mathematical statement in a small subset of mathematics (arithmetic on some finite subset of integers and rationals) and produces an output.
So we can take a partial mathematical statement 3 + 4 and use it, in conjunction with a calculator, as a program that produces the output 7.
So finally, we can answer your question. TLC is a program that's more sophisticated than ordinary calculators, and we can certainly write some mathematical statements in a subset of TLA+ so that when we feed them into TLC we create some interesting output. It is similar to a CAD/CAM tool you run on an architectural blueprint. But is the tool "an implementation" of the blueprint? I don't think that makes sense.
> At what point is there sufficient programming language functionality for you to become convinced that TLC is a programming language?
TLC is not a language but a tool that can process a subset of TLA+. The existence of calculators or of TLC does not mean that mathematics is a programming language, because:
1. Even though mathematics can be used to describe all programs and all of physics -- because the domain describable by mathematics, and therefore by TLA+ -- is a superset of all the behaviours of physical and computable things, it is also a strict superset, and mathematics (and therefore TLA+) can describe lots and lots of things that cannot possibly be realised by anything in the physical world or by any computation.
2. Even though some subset of mathematics (and therefore of TLA+) can be used in conjunction with some program to produce an intended output, that output is not the purpose of mathematics (and therefore of TLA+).
As for 1, you may then ask what's the point of a language that is ultimately intended to produce designs for physically-realisable systems to encompass all of mathematics and describe things that are not realisable. There are two answers to that: first, it makes the working with the language much simpler, just as working in classical mathematics is simpler than working in constructive mathematics (which is based on intuitionistic or some other constructive logic rather than classical logic). Second (and this is really an application of the first answer), specifying non-realisable things is helpful when specifying properties of realisable things. For example, suppose you design an algorithm that can decide whether some specific subset of programs halt. You want to check the proposition that:
InMySubset(InputProgram) ⇒ MyAlgorithm(InputProgram) = Halts(InputProgram)
I see that again and again you're getting stuck on the point that because there are programs that can evaluate mathematical statements, mathematics is a programming language. But the fact that you can describe any program or any physical system in mathematics is the point and power of mathematics. But mathematics is neither physics nor programming because it can also describe things outside the world of programs and physics.
Of course you can write programs in every rich mathematical formalism, including TLA+ (and TLC has nothing to do with it; this would be true even if TLC didn't exist). But programming languages are languages that can describe things that live in a small subset of the world of mathematics. TLA+ is not a programming language not because it doesn't contain the universe of all programs -- it does; every imaginable program could be specified in mathematics and specifically in TLA+ -- but because it contains much, much more.
So if you want to define "a programming language" as any language in which you could describe many or perhaps even all computations, then every rich mathematical formalism (and therefore TLA+) could be considered a programming language. But I would think that a language where most things you write are not computable isn't a programming language. Rather, a programming language is one where everything you write in the language is at the very least computable, and that is certainly not the case for TLA+.
Something similar is true for English. You can use English to describe any conceivable algorithm, and there are now tools that could convert a subset of such descriptions to executable software. But the fact you can use English to describe programs doesn't make English a programming language, because many of the things it is used to described aren't programs.
But even if you insist that mathematics (or English) is a programming language, the point is still that mathematics (and TLA+) exists to describe useful things that go well beyond what could be described in a programming language [1].
[1]: Halts(Program, vars) ≜ Program ⇒ ⬦□(vars' = vars)
[2]: I'm overlooking the type level in programming languages with rich type systems (like Agda), but the point still stands, only the details are more technical.
- TLA+ is "definitely not" a programming language (per you and Leslie Lamport).
- TLC has got nothing to do with TLA+ (as a mathematical formalism). TLC is not "an implementation of TLA+". (per you)
- TLC is a tool that can process "something like" TLA+. You say "subset", but it seems to me it is not a strict subset, because special operators like "Print" have different semantics. Let's suggestively call what it processes "TLA-PL". You mention additional configuration but the configuration can be empty so it's really like a pragma or compiler option.
- TLC can evaluate and print TLA-PL expressions in a REPL. (per the repo I linked)
- TLC and TLA-PL could be extended to implement typical programming language primitives such as input, a Java FFI, etc., fairly easily (per observation of the source code)
- TLA-PL is not TLA+, because it is not a rich mathematical formalism, like a drawing tool or English. The purpose of a TLA-PL document ("program") is to produce an output that's either TRUE or a counterexample, although there are other modes of running TLA-PL. In contrast, the purpose of TLA+ is itself, and a TLA+ document ("specification") has no output - the deliverable is the document.
Now it is true that other programs have REPL-like functionality, like the calculator you mention. Generally the benchmark between calculation and programming is Turing completeness, e.g. whether the language can express recursion. In a calculator, if you add a few statements like stack push/pop and command names, suddenly it is a "programmable" calculator like the HP-32S, and Turing complete, and the calculation language becomes a programming language. What about TLA-PL? Naturally TLA-PL expresses recursive statements easily - it is almost trivially Turing complete and hence a programming language. And it is clear by definition that TLC is an interpreter for TLA-PL, so TLA-PL is even an implemented programming language. This is what distinguishes it from the majority of formalisms, in that most formalisms (English, mathematics), although potentially usable for programming, do not have working implementations. It is not a requirement to be a programming language that everything written in the language is computable - Verilog, for example, is actually quite flexible as a hardware synthesis language, allowing one to write unsynthesizable programs, but in practice people simply avoid writing these programs when doing hardware synthesis. Similarly I am sure that valid-looking TLA-PL programs will look correct but nonetheless fail to run under TLC due to limitations of the model checking and so on.
Now it is true that TLC, although it implements TLA-PL, is not an implementation of TLA+, as by definition TLA+ is like mathematics, infinite in scope, hence not implementable. I would argue this also means TLA+ also isn't even definable, but that's a separate issue. Similarly, Leslie Lamport's purpose in creating TLA+ was not (and is not) to create the programming language TLA-PL, even though it exists. This to me is what you're getting stuck on. As a programming language designer, what I care about is TLA-PL. To me it is clear as day that TLA-PL exists as a programming language and and could be turned into a useful one given sufficient effort to modify TLC. In contrast, all I hear from you is "TLA+ this", "TLA+ that", "pay no attention to the working implementation of TLA-PL". But as I said, I don't care about TLA+ - as soon as you say it realizes unrealizable things, you are speaking poetry rather than programming language design. There are tricks like lazy evaluation and so on where a computer represents "unrepresentable" objects symbolically and thus can manipulate them, and from my understanding some of these tricks are implemented in TLC and TLAPS, but it seems clear you are talking about a level beyond this, where a TLA+ specification cannot be evaluated even with symbolic tricks.
> as soon as you say it realizes unrealizable things, you are speaking poetry rather than programming language design
No! Because the purpose of TLA+ is not to build executable things but to help design and reason about executable things, and it turns out that being able to describe non-executable things is very useful for that purpose (as I tried to show with the Halts example). The ability of a mathematical specification language like TLA+ to describe unrealisable things is the source of its power to succinctly and clearly specify realisable things, because a description of something is not the thing itself.
It's like saying I'm not interested in mathematics, only the subset that can describe physical things. But it turns out that restricting mathematics to physical things makes it more difficult to work with.
This isn't poetry, just the practical realities of mathematics.
> TLC
I think your focus on TLC is a distraction because even when your TLA+ specification does describe a computable process, TLC doesn't actually run that process (it can be put in a mode that does, but that's actually more confusing here). TLC behaves more like a sophisticated type-checker. Type checkers are extremely useful (and TLC even more so) when reasoning about a computational system, and some clever people have found ways to program them to produce interesting outputs, but that's not really what you have in mind when you think about running a program.
For example, TLC can check and verify in an instant a specification of an uncountably infinite number of executions, each of infinite length, and yet choke on a specification of only a few possible instances of, say, QuickSort.
> it seems clear you are talking about a level beyond this, where a TLA+ specification cannot be evaluated even with symbolic tricks.
Yes, but even that is not the point. You seem to be very focused on execution, programming, and evaluation, and these are not the things that TLA+ helps with.
There is no doubt that a programming language is more useful than a mathematical specification for producing software -- because you can build software without a mathematical specification but not without a program -- just as a hammer is more useful than a blueprint when building a cabin, as you can build the cabin without a blueprint, but not without a hammer. But asking how to fashion the blueprint into a hammer misses its point.
Consider this mathematical description of the vertical motion of a projectile thrown from ground level:
y = v0*t + 0.5gt^2
The purpose of TLA+ is to write a small specification of the relevant details of a 5MLOC program, and use it to answer questions such as "can network faults lead to a loss of data?" Sure, running the program is the ultimate goal, but being able to answer such questions can be extremely helpful, and is hard to do with a detailed description that's 5 million lines long.
Now, it's perfectly fine to say that you don't care about such capabilities, but these are the capabilities that TLA+ exists to give.
There are languages out there that aim to do both -- produce an executable and offer advanced reasoning capabilities -- but these languages usually turn out to be much more difficult to program with than traditional programming languages and harder to reason with than with TLA+.
> execution - [this is not one of] the things that TLA+ helps with.
I think there is a depth limit on HN so I'm just going to stop after this. No, I do not have a "real question". I made a statement, that TLA-PL is a programming language. You still not have agreed or disagreed with this statement, just said that you find it "a distraction" and "confusing" and "not really what you have in mind". Well, un-confuse yourself and present an opinion on its veracity. I don't think it's a distraction because it is a point Lamport brought up in TFA.
It is a programming language only the same sense that some subset of English that you could interpret as instructions is a programming language. It's not that you can say, if you only use these symbols then you'd get something executable. While a language could technically be defined like that (a language is just a set of strings), programming languages (and all practical formal languages) are usually defined in a way that it is very easy to mechanically determine whether or not something is in the language and even have a generative grammar for it.
But yes, it is true that are subsets of rich mathematical formalisms (including TLA+) as well as of English that could be "executable", but these subsets are not as easily recognised. So it's a matter of how you define a programming language. If you consider "the subset of English that could be interpreted as a program" to be a programming language, then yes, such subsets of mathematical formalisms including TLA+ exist. If you also require that a programming language is a language that should be easy to decide whether some string is in the language or not, then you'd have to restrict the subset to be very small (just as it is easy to decide the subset of mathematical expressions that can be evaluated by a calculator), and then it's again up to you whether or not you would consider something so rudimentary to be a programming language.
To be more specific, I would not consider the subset of TLA+ that can be simulated or checked by TLC in a way that you'd want an interpreter for a programming language to behave to be a programming language because that subset is not easy to define. For example, you could have two specification of the same program, both of which in the subset that TLC supports, and yet TLC would exhibit a behaviour that could resemble an "execution" for one and not terminate for the other -- even though their meaning is identical. That is because TLC performs a certain analysis of the specification to determine whether some propositions are true or false (e.g. a proposition that a certain variable is always of the same "type") and the algorithm used by that analysis sometimes resembles how people would imagine an interpreter to work and sometimes it doesn't.
So I would say that that subset, like a similar subset of English, is more "a language that could be used to produce a program" than "a programming language" because it is neither as well-defined nor as well-behaved as what we expect from a programming language.
On the other hand, there is an even smaller subset of the language than the one supported by TLC, which could be easily defined, well behaved, and guaranteed to be executable, but it would be quite limited and not make a useful programming language. You can still call it a programming language, but again, it would be smaller than the subset TLC supports.
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 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.
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.
Almost spit out my drink dude, no jokes this early in the day.
That doesn't mean that it's easy, or easier, or that it feels more familiar to a programmer. These are different things.
> 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.
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.
Where is the outline for English? French has a more structured oversight with organizations and goals, so it will beat English?
Even the most popular languages such as Python have just a few viable implementations.
Roadmap/focus is useful in a collaboration.
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]
f :: Integer -> Integer
f x = -(f x)
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.
> 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]
Why is this original definition different than say
f ≜ CHOOSE f ∈ [Int → Int]:
∀ x ∈ Int : f[x] = 0
You didn't realise that f[x] = -f[x] implies f[x] = 0, and that is how it is often: You have some property, but you don't know what it entails exactly. TLA+ allows you to reason about that.
THEOREM fIsTheZeroFunction ≜
f = [x ∈ Int ↦ 0]
PROOF
⟨1⟩ DEFINE zero[x ∈ Int] ≜ 0
⟨1⟩1. ∃ g ∈ [Int → Int] : ∀ x ∈ Int : g[x] = -g[x] BY zero ∈ [Int → Int]
⟨1⟩2. ∀ g ∈ [Int → Int] : (∀ x ∈ Int : g[x] = -g[x]) ⇒ g = zero OBVIOUS
⟨1⟩3. QED BY ⟨1⟩1, ⟨1⟩2 DEF f
You can then use that proof like so:
THEOREM f[23409873848726346824] = 0
BY fIsTheZeroFunction
Writing deductive proofs like above can be tedious when they're not so simple, and the TLA+ toolbox contains another tool, called TLC, that can automatically verify certain propositions (with some caveats), especially those that arise when specifying computer systems (though it cannot automatically prove that f is zero everywhere).
So the purpose of my example wasn't to show something that is useful for engineers in and of itself, but to show that TLA+ works very differently from programming languages, and it is useful for different things: not to create running software but to answer important questions about software.
Thanks again!
There are other good resources (some somewhat updated, but not enough to matter) are listed here: https://lamport.azurewebsites.net/tla/learning.html
def f(x):
return -xI 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?
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
A(x, y)' = 3
def f(x):
return -f(x)
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
def Inc(x):
return x + 1
3 = Inc(x)'
3 = (x + 1)'
3 = x' + 1
2 = x'
x' = 2
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).
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.
By "specification language" Lamport means one capable of verification via model checking.
In contrast, "programming languages" are not capable of such verification.