[pron]

> Is TLA+ simple? I find this hard to accept.

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.

[zekrioca]

> It is very, very simple, and I would say easier to learn than Python, as long as you remember that it is not programming but maths. For example, suppose you specify this function on the integers:

> f ≜ CHOOSE f ∈ [Int → Int] : > ∀ x ∈ Int : f[x] = -f[x]

> What function is it? Clearly, it's the zero function

Did you mean your example is the constant function [1], rather than a zero function [2] (where c = 0)?

[1] https://mathworld.wolfram.com/ConstantFunction.html

[2] https://mathworld.wolfram.com/ZeroFunction.html

[pron]

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

[zekrioca]

Doesn't ℤ include negative natural numbers?

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

[Jtsummers]

The original from pron:

    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.

[zekrioca]

That’s true, my mistake. Thank you for the clarification! In this case, I have another question.

Why is this original definition different than say

f ≜ CHOOSE f ∈ [Int → Int]:

       ∀ x ∈ Int : f[x] = 0

If you want some function to be 0, just specify it. Why does one need to find this a broader but more complex way of specifying the possible “input” space in TLA+? How does it help is my question, I guess.

[pron]

Because sometimes you're not sure if your belief is correct. To show what TLA+ can do, I used a simple example where the truth of the proposition (f is the zero function) is pretty obvious yet behaves very differently from how programming works to show how you can prove things in TLA+:

    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

The TLAPS TLA+ proof-checker verifies this proof instantly.

You can then use that proof like so:

    THEOREM f[23409873848726346824] = 0 
       BY fIsTheZeroFunction

But when you specify a non-trivial thing, say a distributed system, you want to make sure that your proposition -- say, that no data can be lost even in the face of a faulty network and crashing machines -- is true but you're not sure of it in advance.

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.

[auggierose]

This was just an example that TLA+ is not executable.

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.

[pistoleer]

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

    def f(x):
        return -x

[hwayne]

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.

[bvrmn]

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.

[pistoleer]

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?

[bvrmn]

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.

[pron]

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

[pron]

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