The Future of TLA+ [pdf]

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.

While I agree with you on the general idea, I think this is too restrictive:

> A specification language does not tell a machine what operations to perform, a programming language does.

There is a style of programming (usually functional or relational programming) that does not bother itself with operations, and which aims to merely describe a result. Specifications are still different from implementations written in such a style of programming.

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

Oh, if you define specification as something that should be done by people without a PhD, you might have a point.

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.

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