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