And I wonder if TLAPLUS is well suited to functional programming.
I know that Leslie says that it is possible. I'm dubious.
I can't imagine that I said that, since I know almost nothing about
functional programming. I know what a mathematical function is--for
example, it is traditionally defined as a set of ordered pairs. But
programming is about computation and a set of ordered pairs says
nothing about computation. I gather that in purely functional
programming one actually describes a function (an ordered pair of
states) in a way that suggests how it can be computed. You can write
functions that way in TLA+, but I don't know if there's any advantage
to doing that rather than writing them in a functional language. Since
TLA+ allows writing things in ways that don't suggest how they can be
computed in practice, I suspect that it might be good for specifying
the function to be computed by a functional program. But I have no
practical experience with this.
In general, concurrent programs need to be described in terms of how
they change the state. I presume that a purely functional language
has no concept of state, so I don't know how people write such
programs in "functional" languages. Martin seems to suggest that
"functional" languages are used for concurrent programs by specifying
the next-state relation as a set of functions, each specifying a
possible state transition. This isn't a good way to write
higher-level specifications, which require relations rather than
functions, but it might be fine for writing programs. In any event, I
have never seen any published description of a concurrent algorithm
that claims to be written "functionally"; all the ones I've seen are
written using non-functional concepts like assignment. They're usually
written too informally for it to be meaningful to say that they are
using a functional language in the descriptions.
I find Martin's statement
a purely functional language like Haskell, which is closer to logic
... and better suited to reasoning about parallelism
rather puzzling. I think what he means is that if you'rer computing a
function, writing it in a functional language makes it easier to see
how parallelism can be used to speed up the computation of the
function. While of great practical importance, this kind of
parallelism represents a subclass of concurrency (which can be
rigorously defined) that is very simple. (I believe that Map Reduce
is a language for describing that class of algorithm.) In particular,
avoiding errors in such parallel algorithms is no more difficult than
avoiding them in sequential algorithms, so it hasn't interested me
very much.
Leslie