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

[pete.h...@xxxxxxxxx]

This is an old thread, but it is Christmas. Rooting among some old bookmarks I remembered it.

I think TLA is no less relevant if you are implementing something in a functional programming language -- that is, where "something" means something that interacts with the rest of the universe.  

As functional programmers, we have type-theoretical gadgets like 

io-primitive : Input -> IO Output

that tell us where effects might not occur, with luck. But what we don't have is anything that tells us what these effects might be, ie. what can be assumed about them when figuring out a system. 

Personally, I find state-variables, predicates over them, relations over different ones, and the machinery of TLA to be (among) the best way I know of writing down important properties of effect-exhibiting behaviours.  

All programming is fetch-execute. The only difference with functional-programmin is that FETCH involves evaluating an IO-program to normal form, and EXECUTE involves building the next thing to execute out of the environments response.