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