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

Why is a (purely) functional program not considered a system? Does
system imply state transitioning?

I used the term system incorrectly. Let's define a property as a
collection of behaviors. Any property can be specified by a TLA+
formula. A system is a property in which every step of every behavior
can be considered either a step of the system or a step of its
environment. A functional system is in which every (non-stuttering)
behavior consists of two steps--an environment step that provides
input to the system followed by a system step that returns an output
to the environment, such that there is a function that maps input

to output. Such a system can be described by that function.

Why is a (purely) functional program not considered a system?
Does system imply state transitioning?

A program is something that gets executed on a computer. A program
can be described as a state machine--something specified by a TLA
formula Init /\ [][Next]_vars. A functional language is a particular
way of writing programs. A purely functional language, which can
implement only functional specifications, allows a lot of freedom to a
compiler--arguments can be evaluated in arbitrary order, it can
perform common subexpression elimination, etc. This means that

- It is probably inconvenient to describe the meaning of
such a program as a state machine.

- Different compilers can translate the same purely functional
program into code with very different computational complexity.

Those two observations are not unrelated.

one can wrap a pure function interface over an imperative
algorithm

An algorithm is a collection of behaviors. I presume by an imperative
algorithm you mean one described in an imperative language, or as
a TLA formula Init /\ [][Next]_vars. I don't know what it means to
wrap an interface over an algorithm. Perhaps you mean that the algorithm
can implement a functional property. In TLA, that means that the
specification obtained from Init /\ [][Next]_vars by hiding all
the variables except those that describe the communication between
the system and its environment--the specification written

\EE some_vars : Init /\ [][Next]_vars

implies the functional specification (the one the allows behaviors with
those two non-stuttering steps).

What all this boils down to is that functional programs (ones that
just compute a function) are a particular subclass of systems. Since
all systems can be described in TLA by temporal formulas, this
subclass can as well. However, that doesn't mean that it's a useful
way of describing that subclass.

I'm sorry if this is incoherent, I don't have time to try to make
it clearer.

Leslie