TL;DR: Of course TLA+ can be used to describe all programs, as can all sufficiently-rich mathematical formalisms (regardless of TLC; TLC has got nothing to do with that). It is definitely not a programming language because its expressive power comes from its ability to describe things that cannot be computed (or practically computed). I.e. it's not a programming language not because it's too small of a subset of programming, but rather a vastly larger superset of programming. In other words, TLA+ (and mathematics in general) is not a programming language not because it is less than a programming language but because it is more. If TLA+ is a programming language, then so is any rich mathematical formalism, any drawing tool, or English for that matter.

> Is TLC a programming language implementation or not?

Ok, so first of all, TLC is not "an implementation of TLA+" and not because it can only check a limited subset of TLA+.

To sho that, let me take a short but important detour. What is the purpose of a computer program? It is to produce an output, either for yourself or for others you give the program to. In contrast, what is the purpose of a TLA+ specification, i.e. what is it that you do with it, or what is the deliverable? Clearly, it's not some output because a TLA+ specification has no output (I'll get back to TLC in a moment). Once you're convinced that the TLA+ specification fulfils the propositions you're interested in -- either by inspection, formal manipulation and proof on paper, formal proof checked by TLAPS, or a successful run of TLC -- the deliverable is the TLA+ specification itself, the set of formulas, whose purpose is then for someone (maybe yourself or someone else) to use as a design for some system to build -- a program, a computer chip etc.. So a the purpose and deliverable of a TLA+ specification is it itself, just like the purpose of an architectural blueprint.

Now, back to TLC. TLC is, no doubt, a program that takes as an input a TLA+ specification written in a particular subset of TLA+ and some additional configuration that defines the boundaries of state space to model-check, and produces an output that's either TRUE or a counterexample. There are other modes of running TLC, as well, for which special operators like PrintT can be useful.

Note that there are many other programs that do something with a piece of mathematics and produce an answer. The simplest one is a calculator. A calculator is a program that takes as an input some portion of a mathematical statement in a small subset of mathematics (arithmetic on some finite subset of integers and rationals) and produces an output.

So we can take a partial mathematical statement 3 + 4 and use it, in conjunction with a calculator, as a program that produces the output 7.

So finally, we can answer your question. TLC is a program that's more sophisticated than ordinary calculators, and we can certainly write some mathematical statements in a subset of TLA+ so that when we feed them into TLC we create some interesting output. It is similar to a CAD/CAM tool you run on an architectural blueprint. But is the tool "an implementation" of the blueprint? I don't think that makes sense.

> At what point is there sufficient programming language functionality for you to become convinced that TLC is a programming language?

TLC is not a language but a tool that can process a subset of TLA+. The existence of calculators or of TLC does not mean that mathematics is a programming language, because:

1. Even though mathematics can be used to describe all programs and all of physics -- because the domain describable by mathematics, and therefore by TLA+ -- is a superset of all the behaviours of physical and computable things, it is also a strict superset, and mathematics (and therefore TLA+) can describe lots and lots of things that cannot possibly be realised by anything in the physical world or by any computation.

2. Even though some subset of mathematics (and therefore of TLA+) can be used in conjunction with some program to produce an intended output, that output is not the purpose of mathematics (and therefore of TLA+).

As for 1, you may then ask what's the point of a language that is ultimately intended to produce designs for physically-realisable systems to encompass all of mathematics and describe things that are not realisable. There are two answers to that: first, it makes the working with the language much simpler, just as working in classical mathematics is simpler than working in constructive mathematics (which is based on intuitionistic or some other constructive logic rather than classical logic). Second (and this is really an application of the first answer), specifying non-realisable things is helpful when specifying properties of realisable things. For example, suppose you design an algorithm that can decide whether some specific subset of programs halt. You want to check the proposition that:

InMySubset(InputProgram) ⇒ MyAlgorithm(InputProgram) = Halts(InputProgram)

and to do that you need to describe the operator Halts even though it is not realisable (as it's not computable). So Halts clearly cannot be written as a program, yet defining it in some mathematical formalism is needed to express a real property of a real program. (BTW, the definition of a Halts operator is a trivial one-liner in TLA+ [1]).

I see that again and again you're getting stuck on the point that because there are programs that can evaluate mathematical statements, mathematics is a programming language. But the fact that you can describe any program or any physical system in mathematics is the point and power of mathematics. But mathematics is neither physics nor programming because it can also describe things outside the world of programs and physics.

Of course you can write programs in every rich mathematical formalism, including TLA+ (and TLC has nothing to do with it; this would be true even if TLC didn't exist). But programming languages are languages that can describe things that live in a small subset of the world of mathematics. TLA+ is not a programming language not because it doesn't contain the universe of all programs -- it does; every imaginable program could be specified in mathematics and specifically in TLA+ -- but because it contains much, much more.

So if you want to define "a programming language" as any language in which you could describe many or perhaps even all computations, then every rich mathematical formalism (and therefore TLA+) could be considered a programming language. But I would think that a language where most things you write are not computable isn't a programming language. Rather, a programming language is one where everything you write in the language is at the very least computable, and that is certainly not the case for TLA+.

Something similar is true for English. You can use English to describe any conceivable algorithm, and there are now tools that could convert a subset of such descriptions to executable software. But the fact you can use English to describe programs doesn't make English a programming language, because many of the things it is used to described aren't programs.

But even if you insist that mathematics (or English) is a programming language, the point is still that mathematics (and TLA+) exists to describe useful things that go well beyond what could be described in a programming language [1].

[1]: Halts(Program, vars) ≜ Program ⇒ ⬦□(vars' = vars)

[2]: I'm overlooking the type level in programming languages with rich type systems (like Agda), but the point still stands, only the details are more technical.