The Future of TLA+ [pdf] (opens in new tab)

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!".

Exactly my thoughts as well.

So for us normies does that mean skip TLA?

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?

Sounds similar to UML: Unified Modeling Language diagrams.

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

Are there any RFCs written in TLA+?

> Math is a natural language

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

> 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.

Coq is not a specification language. It’s an interactive theorem prover. The goal set is completely different.

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

A more interesting example would be

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.

Assuming you meant to write,

    def f(x):
        return -f(x)

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).