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

[George Singer]

I’m trying to understand if TLA+ is useful if your primary implementation language is a functional one like Haskell. So I’m going to make some assertions and come to a conclusion, in the hopes that people will point out where I’m going wrong or right. I’m half-way through the TLA+ book, so I apologize if I get some things wrong.

1 My Understanding of TLA+ Specs

Specs in TLA+ take the form of temporal formulas with the following structure:

Spec == Init /\ [][Next]_vars /\ Liveness

Here, Spec can be said to be satisfied by a certain class of behaviors. Behaviors are a sequence of states. Crucially, a state is a set of variables whose values can change over time.

2 Purely Functional Programs Reduce TLA+ Specs to Non-Temporal Formulas

Functional languages like Haskell heavily discourage the use of variable mutation. So is this a problem for TLA+?

There are two cases to analyze.

First case: The first case is when you are breaking the rules of Haskell, and introducing mutable state into your program anyway. In Haskell this is discouraged but allowed. Well, in this easy case, TLA+ can help you reason about your partially stateful program as usual (i.e., TLA+ will be just as useful to you had you written your program in C or Java).

Second case: Now suppose your program is completely pure. What then is the use of TLA+? It seems to me that the following would be true:

• All actions of form (x = x') would be trivially satisfied by all behaviors.
• Thinking in terms of actions is therefore not helpful (for such purely functional programs).
• Conjuncts of form [][Next]_vars /\ Liveness can therefore be stripped from TLA+ specs, since they cannot express any interesting properties (i.e., they will either be vacuously true or false).

Thus, if you are writing a purely functional program, all of your TLA+ specs will be purely non-temporal, in the sense that they will take the form of first-order logic sentences with no temporal symbols like [] or apostrophe. But, I conclude, writing such a spec will still be helpful, for it will force you to reason about the properties of your (purely functional) program in the mathematical language of first-order logic. This is because it will force you to think of your program at a higher-level than even Haskell.

3 Conclusion: TLA+ is Still Useful to Functional Programmers

If your program is purely functional, then TLA+ forces you to write a non-temporal spec. But reducing your spec to a non-temporal formula still forces you to think and write in terms of math (i.e., first-order logic and set theory), which seems useful. Finally, if your functional program requires the use of mutable state anyway (which can be done in Haskell, despite being discouraged), then a TLA+ spec will be just as useful to you had you written your program in a non-functional language like Java or C.

So do people think this line of reasoning is sound?

​

[Leslie Lamport]

I find your argument sound, though the subject of the posting is
misleading.  As you make clear, the language you're using is
irrelevant.  It's whether you're writing a simple functional program
or a reactive program--that is, implementing a system.

You should mention that the TLA+ tools were not optimized for
evaluating functions.  While writing a mathematical specification of a
functional program may help you understand what you're doing, the
tools might not be useful in helping you to debug it.  If the tools
can't find errors in your spec, you might be better off writing an
informal spec rather than a formal TLA+ spec.

A benefit of using TLA+ is that it teaches you to think
mathematically, which teaches you to write better informal specs.  In
particular, it teaches you to think above the code level--meaning at a
level at which the language you're using is irrelevant.  An example
is the TLA+ pretty-printer in my lecture "Programming Should be More
than Coding", which is at

  https://www.youtube.com/watch?v=6QsTfL-uXd8

One other possible use of TLA+ for functional programs that you didn't
mention is in coming up with an algorithm to compute the function.
The complexity of an algorithm is how many steps it takes to execute.
The complexity of a function is the smallest number of steps it takes
to compute it.  That's not a practically useful concept of complexity.
The complexity of sorting is N log N, but if I write bubble sort in a
functional language, the complexity of the function I've defined is
N log N, but no compiler is going to produce a program with that
complexity.  I expect that there are many algorithms that are easier
to think of imperatively than functionally.  It may be because
I'm used to programming imperatively.

Leslie

[George Singer]

Leslie — I’m watching the video you posted. It’s great.

As you make clear, the language you’re using is
irrelevant. It’s whether you’re writing a simple functional program

or a reactive program—that is, implementing a system.

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

One other possible use of TLA+ for functional programs that you didn’t
mention is in coming up with an algorithm to compute the function.
The complexity of an algorithm is how many steps it takes to execute.
The complexity of a function is the smallest number of steps it takes
to compute it. That’s not a practically useful concept of complexity.
The complexity of sorting is N log N, but if I write bubble sort in a
functional language, the complexity of the function I’ve defined is
N log N, but no compiler is going to produce a program with that
complexity. I expect that there are many algorithms that are easier
to think of imperatively than functionally. It may be because
I’m used to programming imperatively.

I’m assuming here your point is that (as it relates to TLA+), in a purely functional language, one can wrap a pure function interface over an imperative algorithm and, when doing so, use TLA+ to help specify various safety and liveness properties of the algorithm.

[Leslie Lamport]

   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

[Hillel Wayne]

There's a couple of immediate cases I can see where TLA+ is still handy here:

1. While your code may be pure, if it does any sort of IO there's a high likelihood that it's affected by some outside state. For example, it might make API calls or read data from a database. In that case, TLA+ can be used to spec the total system, with the assumption that the all of the Haskell code runs in a single step.

2. If your code has no mutability whatsoever, you can try using TLA+ as an oracle. As a trivial example, let's say you write an algorithm to find the maximum number in a set. In TLA+, the "maximum number of a set" is just

Max(S) == CHOOSE x \in S : \A y \in S : y <= x

So you can implement the algorithm in TLA+ and then specify the invariant

\A S \in SUBSET Int : MyMaxAlgorithm(S) = Max(S)

To see if it's correct.

That said, TLA+ is designed for temporal systems, and while it can handle stateless systems, there are probably better tools out there for that. I've heard that Alloy is pretty good but haven't tried it myself.

[pete.h...@gmail.com]

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.

[Ron Pressler]

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.

​

[Ron Pressler]

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

[Peter Hancock]

Ron,

Thanks for your comments, that deserve a more detailed response than I can give right now.

I'd like to understand better "where you are coming from". Broadly speaking, it seems
that faced with a specification, about the part of the universe that one wants to get
to behave in a certain way (say, the contents of a terminal open on my display, or where
a piece of artillery points in the sky), it doesn't a priori matter whether one decides
that a computer should be involved, let alone what kind of programming language one
should write the code in to load into that computer. Do('nt) you agree? It might
be a bunch of people in a room with slide rules, passing around numbers written on post-its,
finally telling the gunners where to point their weapon.

There seems to be something highly distracting about functional programming, that
reminds me of those occasions when I look all over the house for my glasses and
then find them on my nose. If we spend a lot of time in a REPL loop, as in ghci,
we get so fascinated by the "E" that we forget about the "R" and the "P".

I'd like to think that "programming" is essentially a matter of figuring out how
to bring about desired behaviours, and avoid bringing about undesired ones.
In real life though, as we all know, "programming" is often a matter of
clarifying and understanding a specification, and ruefully asking ourselves whether
it really captures anything intelligible a sensible person might intend.
It seems to me one of the great benefits of decades of work on specification,
TLA+, predicate transformers or whatever, is that it rubs our noses
in this "sharp end" of programming.

There's a lot to be said about how one figures out a candidate implementation of
a specification using a functional programming language, how type systems might help
or hinder. Personally, this stuff fascinates me, and I'd be delighted to discuss it with
you (though it probably shouldn't be in this forum!).

My remarks above seem to me rather anodyne and unexceptional, no doubt
could be better expressed, and I may have entirely missed your point(s?).
Have I said something you take exception to?

With respect,
Peter Hancock

[Ron Pressler]

I agree with everything you've said, and I, too, think that pure-FP in particular is distracting in the sense that it draws much attention to the language, or the form of expression, at the expense of what is being expressed. In that way, TLA+ is (at least in spirit) the opposite.

Ron