I find your argument sound, though the subject of the posting is
misleading. As you make clear, the language you're using is
irrelevant. It's whether you're writing a simple functional program
or a reactive program--that is, implementing a system.
You should mention that the TLA+ tools were not optimized for
evaluating functions. While writing a mathematical specification of a
functional program may help you understand what you're doing, the
tools might not be useful in helping you to debug it. If the tools
can't find errors in your spec, you might be better off writing an
informal spec rather than a formal TLA+ spec.
A benefit of using TLA+ is that it teaches you to think
mathematically, which teaches you to write better informal specs. In
particular, it teaches you to think above the code level--meaning at a
level at which the language you're using is irrelevant. An example
is the TLA+ pretty-printer in my lecture "Programming Should be More
than Coding", which is at
https://www.youtube.com/watch?v=6QsTfL-uXd8
One other possible use of TLA+ for functional programs that you didn't
mention is in coming up with an algorithm to compute the function.
The complexity of an algorithm is how many steps it takes to execute.
The complexity of a function is the smallest number of steps it takes
to compute it. That's not a practically useful concept of complexity.
The complexity of sorting is N log N, but if I write bubble sort in a
functional language, the complexity of the function I've defined is
N log N, but no compiler is going to produce a program with that
complexity. I expect that there are many algorithms that are easier
to think of imperatively than functionally. It may be because
I'm used to programming imperatively.
Leslie