I’m trying to understand if TLA+ is useful if your primary implementation language is a functional one like Haskell. So I’m going to make some assertions and come to a conclusion, in the hopes that people will point out where I’m going wrong or right. I’m half-way through the TLA+ book, so I apologize if I get some things wrong.
Specs in TLA+ take the form of temporal formulas with the following structure:
Spec == Init /\ [Next]_vars /\ Liveness
Spec can be said to be satisfied by a certain class of behaviors. Behaviors are a sequence of states. Crucially, a state is a set of variables whose values can change over time.
Functional languages like Haskell heavily discourage the use of variable mutation. So is this a problem for TLA+?
There are two cases to analyze.
First case: The first case is when you are breaking the rules of Haskell, and introducing mutable state into your program anyway. In Haskell this is discouraged but allowed. Well, in this easy case, TLA+ can help you reason about your partially stateful program as usual (i.e., TLA+ will be just as useful to you had you written your program in C or Java).
Second case: Now suppose your program is completely pure. What then is the use of TLA+? It seems to me that the following would be true:
(x = x')would be trivially satisfied by all behaviors.
[Next]_vars /\ Livenesscan therefore be stripped from TLA+ specs, since they cannot express any interesting properties (i.e., they will either be vacuously true or false).
Thus, if you are writing a purely functional program, all of your TLA+ specs will be purely non-temporal, in the sense that they will take the form of first-order logic sentences with no temporal symbols like  or apostrophe. But, I conclude, writing such a spec will still be helpful, for it will force you to reason about the properties of your (purely functional) program in the mathematical language of first-order logic. This is because it will force you to think of your program at a higher-level than even Haskell.
If your program is purely functional, then TLA+ forces you to write a non-temporal spec. But reducing your spec to a non-temporal formula still forces you to think and write in terms of math (i.e., first-order logic and set theory), which seems useful. Finally, if your functional program requires the use of mutable state anyway (which can be done in Haskell, despite being discouraged), then a TLA+ spec will be just as useful to you had you written your program in a non-functional language like Java or C.
So do people think this line of reasoning is sound?