> Fundamentally no formalism will ever allow you to use more detail than the formalism has

No, because TLA is not a programming language. It's a way to describe computation using math. What you're saying is analogous to saying that there is no way math would allow us to describe physics at arbitrary levels of detail.

> adding those refinements will break symmetries that previously existed

The very definition of refinement is that this can't happen. Formally, if A refines B, then A => B. And so, every feature C of B, i.e., B => C, is also a feature of A, because A => C, due to the transitivity of implication.

> but I think you'd still encounter the same kind of problems if you wanted to model the machine state at a lower level of detail

No, because of universal computation. Once your logic can talk about a single computational step, and thanks to TLA's logical time that then allows you to break that step down further, you really can talk about arbitrary detail. Of course, while true, this is a theoretical possibility. No one is going to actually specify the program at the level of the electrons in the CPU. If someone does, they will encounter a difficulty that isn't about a theoretical limit of formalisms, but one specific to TLA, which is that the logic does not currently allow making probabilistic statements about programs.

> but there will always be finer details not captured in our model.

Sure, in our model -- yes. But not necessarily in our formalism.

> So what I don't see is why you would ever not want the higher-level tools, even if working in a lower-level formalism.

TLA is not a lower-level formalism, although it may sometimes be less convenient for some sequential computations. But because its denotation fully captures the notion of computation, it allows arbitrary levels of detail. Functions are a fundamentally lossy way of speaking about computations; sequences are not. Indeed, sometimes functions are very convenient, but they become not so convenient when concurrency/interaction is involved.

> A lot of the time we are analysing only in terms of denotation (sorted list) rather than operation (bubble sort or merge sort)

Again, you mean in terms of a functional denotation, i.e. the denotation of a function. The denotation of TLA is behavior (a sequence of steps), and while you can easily define an "extensional equivalence" operator on behaviors, one that looks only on the first step (input) and last step (output), the essential denotation in TLA does differentiate between bubble- and merge-sort.

> I'd still want to be able to talk about whether two procedures implemented the same function if the filesystem operated in a certain way.

That's very easy:

ExtensionallyEquivalent(A, B) ≜
∀ x : ∃ y : (A ∧ (input = x) ⇒ ◇□(output = y)) ≣ (B ∧ (input = x) ⇒ ◇□(output = y))

Which means that algorithms A and B are extensionally equivalence if for every input x, A terminates and produces the output y iff B does the same.

> I'd still want monads.

You wouldn't, because, as you've seen, while you can define a weaker equivalence on sequences, there is no need for a special construct to define different kinds of computation. The only reason monads are used in the first place is that functions cannot describe arbitrary non-sequential computation. Monads aren't a "real" feature of computation; they're a tool of a formalism used to describe computation.

It is very important to me to point out that TLA+ is not a programming language. Synchronous languages like Eve, however, do share many of its properties.