> Again, disagree. I think of it more as defining what a sorted list is to the computer. (An extreme example would be doing it in Prolog or the like, where you just tell the computer what it can do and what you want the result to look like).

Exactly, but the point is defining at what level. Take your Prolog example. This is how you can define what a sorted list is in TLA+:

IsSorted(seq) ≜ ∀i,j ∈ 1..Len(seq) : i < j => seq[i] ≤ seq[j]
Sorted(seq) ≜ CHOOSE res ∈ Perms(seq) : IsSorted(s)

So this is a definition, but it's not an algorithm. Yet, in TLA+ it could describe a state machine of sorts: the nondeterministic state machine that somehow yields a sorted list. Any particular sorting algorithm is a refinement of that machine. Of course, the refinement does not need to happen in one step. You can describe a mergesort as a machine that somehow merges, which is a refinement of the magical sorting machine. Any machine that merges, say, using a work area in a separate array, is then a refinement of that. You decide when to stop.

If there's a difference in how you "define" a sorted list via bubble-sort or mergesort in your lookup table image that difference is an abstract state machine. For example, in the mergesort case your composition "arrows" are merges. You have just described a (nondeterministic) state machine. Otherwise, if your lookup table algorithm doesn't have any steps, it must simply map the unsorted array to the sorted array and that's that. If there is any intermediate mappings, those are your transitions.

The state machines are nondeterministic, so you don't need to say "do this then do that". It's more like "this can become that through some transformation". Every transformation arrow is a state transition. You don't need to say in which order they are followed.

Here is a certain refinement level of describing mergesort

∃x, y ∈ sortedSubarrays : x ≠ y ∧ x[2] + 1 = y[1]
∧ array' = Merge(array, x, y)
∧ sortedSubarrays' = {sortedSubarrays \ {x,y}} ∪ {<<x[1], y[2]>>}

That's it; That's the state machine for mergesort (minus the initial condition). It is completely declarative, and it basically says "any two adjacent sorted subarrays may be merged". Note that I didn't specify anything about the order in which subarrays are sorted; this machine is nondeterministic. Even that may be too specific, because I specified that only one pair of subarrays picked at each step. I could have said that any number of pairs is picked, and then my specification would be a refinement of that.

You can define an invariant:

Inv ≜ [](∀x ∈ sortedSubarrays : IsSorted(x))

The box operator [] means "always". Then you can check that

MergeSort => Inv

to assert that the sorted subarrays are indeed all sorted.

> I think/hope we will eventually be able to find a better representation than thinking about it as a state machine directly

There are two requirements: first, the formulation must be able to describe anything we consider an algorithm. Second, the formulation must allow refinement, i.e. the ability to say that a mergesort is an instance of a nondeterministic magical sorting algorithm, and that a sequential or a parallel mergesort are both instances of some nondeterministic mergesort.