[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

You write:

 Crucially, a state is a set of variables whose values can change over time.

but what is meant as state here is not exactly what is meant as mutable state in programming. Here's an example of a (pure) Haskell  function:

gcd :: Int -> Int -> Int
gcd x y = if x == y then x
          else if x > y then gcd (x - y) y 
          else gcd x (y - x)

there is no mutation going on, yet the variables x and y are variables whose values change over time (at each iterative step). It's true that there may not be any mutation of memory addresses (actually, there likely is, because the function is tail-recursive), there is still state. The corresponding TLA+ specification also says nothing about mutation of memory cells. In fact, TLA+ has no notion of memory at all, unless you choose to model it. Variables whose values can change just means that a set of names refers to different values -- this happens in pure functional languages all the time.