Re: Is TLA+ still useful if your implementation language is a purely functional one, like Haskell?

There's a couple of immediate cases I can see where TLA+ is still handy here:

1. While your code may be pure, if it does any sort of IO there's a high likelihood that it's affected by some outside state. For example, it might make API calls or read data from a database. In that case, TLA+ can be used to spec the total system, with the assumption that the all of the Haskell code runs in a single step.

2. If your code has no mutability whatsoever, you can try using TLA+ as an oracle. As a trivial example, let's say you write an algorithm to find the maximum number in a set. In TLA+, the "maximum number of a set" is just

Max(S) == CHOOSE x \in S : \A y \in S : y <= x

So you can implement the algorithm in TLA+ and then specify the invariant

\A S \in SUBSET Int : MyMaxAlgorithm(S) = Max(S)

To see if it's correct.

That said, TLA+ is designed for temporal systems, and while it can handle stateless systems, there are probably better tools out there for that. I've heard that Alloy is pretty good but haven't tried it myself.

On Wednesday, 11 January 2017 12:40:39 UTC-6, George Singer wrote:

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.

1 My Understanding of TLA+ Specs

Specs in TLA+ take the form of temporal formulas with the following structure:
Spec == Init /\ [][Next]_vars /\ Liveness
Here, 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.

2 Purely Functional Programs Reduce TLA+ Specs to Non-Temporal Formulas

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:

All actions of form (x = x') would be trivially satisfied by all behaviors.

Thinking in terms of actions is therefore not helpful (for such purely functional programs).

Conjuncts of form [][Next]_vars /\ Liveness can 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.

3 Conclusion: TLA+ is Still Useful to Functional Programmers

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?