> Even if you're modeling as a state machine, rather than a single big state machine you'd want to separate it into small orthogonal state machines as much as possible.

Your notion of state is too specific for the theoretical meaning. Which function is executing in an FP computation is also state, as is the values of its arguments. Every software system is a single, possibly nondeterministic state machine. The decomposition you speak of is merely a decomposition of the state transition into various chunks (formulas). You can think of an abstract state machine as a single (pure) function -- just like a simple FP program -- except not a function from the input to the output, but a function from one state to the next (kinda like a state monad's monadic function, but expressed more naturally). One last complication is that it isn't quite a function but a relation, as you want to express the fact that your state machine may do one of several things in the next state, e.g. to describe different interleaving of threads, or even to model the user generating input.

Another thing you want to do is refinement and abstraction, i.e. specify your algorithm in different levels of detail (machines with more or fewer states) and show that the properties you want are preserved in the abstraction. Of course, you won't do that for something as simple as a sorting algorithm, but you also want to reason about large complex things, like an OS kernel or a distributed database.

So TLA simplifies things further by saying that the whole world is a single state machine, and your specifications are restricted views of that "world machine". This allows you to specify a clock with minute second hands, and another specification of a clock with just a minute hand, and then say that both are views of the same clock, with the first being just a more refined description of it than the first (this is a problem with multiple state machines, as one takes a step every second, and the other only every minute).

> I see the functional approach as taking that one step further: separate the large proportion of the program that doesn't depend on state at all (i.e. that's conceptually just a great big lookup table - which is the mathematical definition of a function) from the operations that fundamentally interact with state.

Again, what you consider state and the "abstract state" in abstract state machines are not quite the same. There is no such thing as a program that doesn't depend on state. Wherever there's a program, there's state. If you implement an algorithm that finds the maximum element in a list of numbers by a simple traversal in a PFP language and in an impure imperative language, the result would look very different, but the algorithm is the same, hence the state and the state transitions are identical.

That's the whole point in thinking of algorithms, not of code. I'd guess that this is what you do anyway -- regardless of the language. You don't necessarily always reach the same level -- e.g. once your complex distributed blockchain needs to find the maximal number in a list, you may go down to the index level in an imperative language, yet stop at the fold level in FP, and that's fine (you decide what an abstract machine can do at each step) -- but ultimately, at some point, you always think of your algorithm in the abstract -- you see it running in your mind -- rather than in linguistic terms, and that is the interesting level to reason about it. Forget about FSMs. What you imagine is pretty much the abstract state machine you can reason about mathematically. A mathematical state machine is simply a description of your program's steps (and every program is composed of steps) at any level of detail.