[Mathnerd314]

Actually the converse is true: Lean and other projects have formalized most mathematical theorems. But it is an "additive" process - it is easy to paraphrase a formal Lean theorem as colloquial mathematics, but it is hard to formalize colloquial mathematics in Lean. Some of this is due to Lean not being as developed as it could be, but also there is simply that some "theorems" in mathematics are simply "wrong" in that they make unstated assumptions and handwave away important parts of the proof. It is in this sense that programming is less expressive than mathematics, in that you can get away with writing things in mathematics that you can't get through a theorem checker. And this is conversely why I say that programs for theorem checkers are executable - the requirement to pass a theorem checker imposes constraints on proof structure and such that is not found in the "natural" language of mathematics. The lack of these limitations is what I would say the limitation of mathematics is, that even well-known proofs are not necessarily completely "true" due to unstated assumptions.

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.

[pron]

> And this is conversely why I say that programs for theorem checkers are executable - the requirement to pass a theorem checker imposes constraints on proof structure and such that is not found in the "natural" language of mathematics.

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.

[Mathnerd314]

> It's not a program

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

[pron]

> It is a program when I can do java tlatk.TLC someprogram.tla.

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.

[Mathnerd314]

You can write hello world in TLA+:

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.

[pron]

> You can write hello world in TLA+:

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

It has no meaning in TLA+ other than the value TRUE. It's just another way of writing TRUE. The computer program TLC, however, prints some output when it encounters the PrintT operator in a specification, but that behaviour is very much not the meaning that operator has in TLA+. TLC can equally print "hello" whenever it encounters the number 3 in a mathematical formula. There are other TLC tricks that can be used to manipulate it to do clever stuff [2], but that's all specific to TLC and not part of the TLA+ language.

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

It means that a variable named console (which we'll take to represent the content of the console) starts out blank, and at some future point its content becomes "Hello, World!" and it is not changed further.

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

[1]: https://github.com/tlaplus/tlaplus/blob/0dbe98d51d6f05c35630...

[2]: I've even given a talk about such tricks: https://youtu.be/TP3SY0EUV2A

[Mathnerd314]

> the PrintT operator is defined in TLA+ like so

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.

[pron]

P.S.

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.

[hwayne]

I do think there's an interesting and deep connection between the world of model checking and the world of planning (as most often done in logic languages).