P.S.
Of course, a temporal TLA+ specification would model the operational semantics rather the denotational semantics (which are indeed timeless) of a pure functional program. Modeling the denotational semantics is not entirely as straightforward as just using functions, because the denotation of a Haskell "function" of type a -> b (for some specific a, and b) is not a function in [a -> b], but something more complex, as Haskell "functions" represent so-called "partial functions" rather than actual functions. This could be done in TLA+ (by, say, adding a bottom element to all sets and some assumptions about your functions regarding bottom arguments), but, indeed, at some point, the model checker would be of little help.
This is not a limitation particular to TLA+; fully automated verification methods -- whether model checkers or automated SMT solvers -- have difficulty with higher-order-heavy code in general (at least I'm not aware of any tool that can consistently and fully automatically verify complex functional programs employing a lot of higher-order "functions"). There are, of course, proof assistants that work very well with purely functional code, but most of the heavy-lifting is still manual, and they require
a lot of work. On the other hand, modeling the operational semantics even of so-called higher-order programs in TLA+ is pretty straightforward (I tried to show a couple of examples
here).
Ron
On Thursday, January 4, 2018 at 7:38:32 PM UTC, Ron Pressler wrote:
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.