> 1. How do we really get the feel for the benefits of this model? Sure, I can struggle through tutorials on TLA, white papers on Daedalus, and the Eve live demo, but from the little I've seen it's not yet obvious to me how they solve my problems as a day-to-day jobbing programmer. The benefits of Haskell, on the other hand, became clear to me after browsing the Haskell Reddit and noticing that pretty much every post solved a problem I was currently having in my Python codebase.

With respect to TLA+, here's how I'd say it solves problem as a day-to-day jobbing programmer: you know the saying "Weeks of programming can save you hours of planning?" TLA+ is a tool to make planning less tedious and error prone. You can write your plan as a specification, then check if that specification actually meets your required invariants.

If you're expecting to write a couple dozen lines of code, TLA+ is probably not gonna help a lot. If you're expecting to write a couple thousand lines of code, it can save you a ton of pain. But you still have to implement your specification correctly, and that's where things like ADTs can help quite a lot.

> There is a general purpose programming model which supports verification at a very fine grained level, encompassing both computation and effects

Of course there is (synchronous programming), but it may not necessarily be the best fit for all situations, either, and FP may well be more appropriate for sequential programs. Personally, I don't have a problem with not using the "best" at all times. I do have a problem with insisting that some formalism is "best". Like Church wrote, there is simply no such thing.

> I'm a bit puzzled by why you're combative against the Haskell community

My only problem is with claims that either state that Haskell is universally/objectively superior to other approaches because it possesses some property or other or with claims that mistake features of a specific formalism with those of computation in general.

> How do we really get the feel for the benefits of this model? Sure, I can struggle through tutorials on TLA, white papers on Daedalus, and the Eve live demo, but from the little I've seen it's not yet obvious to me how they solve my problems as a day-to-day jobbing programmer.

That's OK. I'm not trying to sell you this approach or make you an advocate for it. I just want people to stop equating FP with "math", as it is certainly not the only "mathematical" approach to programming, nor make claims about its universal superiority.

> The benefits of Haskell, on the other hand, became clear to me after browsing the Haskell Reddit and noticing that pretty much every post solved a problem I was currently having in my Python codebase.

That's great! Haskell works great for some people in some cases, and may not be the best for everyone in every case. You can still advocate for Haskell and tell people how elegant you find the approach and how well it solved your problems. Just don't make universal claims that can't be backed up.

> Does the model you're describing really handle polymorphism and higher order functions?

Polymorphism and higher-order functions are not concepts in computation; they're concepts in functional programming. A model where computations are not represented as functions, obviously has other means of expressing things. For example, dynamical systems are normally expressed using first-order ODEs only, but they can still express any system, even one where the derivative is itself a dynamical process, and so you'd think is a "higher order" system. When you have forms of composition other than function composition, your objects are just different.

Having said that, TLA+ has polymorphism and higher-order functions (only that's not how you represent computation).

> Given that polymorphism and higher order functions are known to be incompatible with set theoretic models I remain sceptical.

I assume you referring to TLA+, which uses set theory as the "data logic". When people say that polymorphism doesn't have a set-theoretic model, they mean that a polymorphic function, say `id :: a -> a`, cannot correspond to a set theoretic function. That doesn't mean it cannot be represented as something else. But, as you're talking about set theory, and so, I assume, referring to formal methods like TLA+, I have to say that I'm not sure at all what the status of polymorphism is in type-theory based proof assistants, which, like TLA+ but unlike Haskell, must be consistent. For example, in Lean, the id "function is:

    universe u
    def id {α : Sort u} (x : α) := x

Now, even after playing with Lean for a few weeks, I'm still not sure what kind of object `id` is, but I'm pretty sure it cannot be a function. The reason for that universe thing is that, unlike in Haskell, you cannot have a type of all types, as, just like in set theory, this leads to contradiction. That is the reason polymorphic "functions" are not set-theoretic functions, but I'm not sure they're type theoretic functions, either. On the other hand, you can have a function that is polymorphic not over all types, but over all types of a certain universe that doesn't include the type of the function itself, but you certainly can represent a polymorphic function like that as a set-theoretic function. So, set theories and type theories are consistent theories, and while I'm not a logician and I could be very wrong about this, I believe that types in consistent type theories do have set models (I know that's the case for Lean, at least).

BTW, if you want to write something similar to the above Lean definition in TLA+, you'd write:

    Id(u) ≜ [x ∈ u ↦ x]

and use it as `Id(Nat)[5]` -- just like in Lean, except the type is not inferred. Of course, you wouldn't do that in practice, as you could simply define

    Id(x) = x

which is polymorphic over all sets. It can do that because it's not a function but an operator.

> > There is a general purpose programming model which supports verification at a very fine grained level, encompassing both computation and effects

> Of course there is (synchronous programming)

So you say! And I'm keeping an open mind on it but I still don't grasp what it's useful for in the life of a day-to-day jobbing programmer like myself.

> Polymorphism and higher-order functions are not concepts in computation

Let's leave polymorphism to one side for a moment, but higher-order "programming"/"computation"/whatever is definitely a concept that's more widely applicable than just in functional programming. Any time you "manipulate a computation" you are doing "higher-order" computation. The universal Turing machine is an example of "higher-order" computation and the proof of the halting lemma requires "higher-order" computation.

Now it's possible that the models you are describing do not allow you to abstract over computation and thus are not "higher-order". If that's the case then either they are weaker than needed to talk about computation in general or they are very remarkable demonstrations that higher-order computation is generally not needed in practice!

> Any time you "manipulate a computation" you are doing "higher-order" computation.

Ah, this is something I specifically address in my TLA+ post series, probably because I heard it come up from you and others. Higher-order is strictly a formal property, i.e., it is a quality of a description of a system, not of a system itself. The best example is from continuous dynamical system. If the derivative of a system is a dynamical system itself, using one formalization you get a higher-order ODE. But people usually prefer describing all dynamical systems using first-order ODEs. The system of equations is first-order, but it still describes a "system that modifies a system". How? Because the "higher-order" function composition can be expressed as first-order composition of a different kind. Instead of writing:

    x'' = 2

you can write:

    x' = y ∧ y' = 2

So this first-order composition corresponds to a higher order system in a world with only one variable.

You don't even have to take my word about TLA. Robin Milner, who was one of the leading advocates and theoreticians of functional programming, moved in the eighties from the lambda calculus to process calculi. He still insisted on algebraic composition, but process calculi are "first-order" yet still equivalent to the lambda calculus. Instead of a function taking a function, you have two processes composed in parallel.

> Now it's possible that the models you are describing do not allow you to abstract over computation and thus are not "higher-order". If that's the case then either they are weaker than needed to talk about computation in general or they are very remarkable demonstrations that higher-order computation is generally not needed in practice!

Not only do they allow to abstract over computation, they organize all computations into a lattice. I.e. if computation b is an abstraction of a (or a is a refinement of b), then a ≤ b in the lattice. So instead of saying that b is a parameterized computation, and that there exists some x s.t. a = b(x), we have that nice order relation; order and nondeterminism are used instead of parameterization. In fact, in TLA this is even used for first-order computations. Instead of saying that F is a computation parameterized by some natural number parameter, we say that F has a "degree of nondeterminism freedom" of a dimension of natural numbers.

That's one of the greatest strengths of such formalisms, as this greatly simplifies formal verification (and one of the reasons why synchronous languages are the languages most amenable so far to formal verification).

Can you give me a concrete example of a higher order computation in TLA? For example, can you show me how to construct a computation that runs another computation over all elements of a list?

It is actually very easy. I cover that in parts 3 and 4 of my series. I will answer your question, but the answer may sound a little tricky. Part of the problem is that simply in stating your question you have quite a few hidden assumptions that are natural in FP but don't take into account how an arbitrary computation can actually behave.

This is an example of a computation that is specifically tailored for functional languages, so let's instead start with something conceptually simpler for TLA, but downright impossible in FP: Plotkin's parallel or. Here you have a computation that takes two arbitrary computations, and simulates them in lockstep. [1]

Doing what you ask is certainly possible in TLA (in part 4), but that's just not how it's normally done. TLA allows you to abstract computations, i.e., extract some of their arbitrary features. As sequential computations of the kind you describe can correspond to functions and can be abstracted into function, that's exactly what you'll do in TLA+. You won't say "my computation runs an arbitrary computation over all elements of a list" (as is possible for Plotkin's or) because in order for that to make sense, that other computation must have certain features and cannot be arbitrary. In particular, it needs to behave like a function. So, what you'll write is a computation that runs something that can be represented as a function over all elements of a list. So, it will simply be:

    CONSTANTS T, R (* the "type" of elements in the in/out list *)
    VARIABLES in, out, f

    Map ≜ ∧ in ∈ Seq(T)
          ∧ f ∈ [T → R]
          ∧ □[∧ out' = Append(out, f[Head(in)])
              ∧ in' = Tail(in)
              ∧ UNCHANGED f]_⟨f, in, out⟩

As you'll note, there are no parameters at all. Instead, we use nondeterminism, i.e., define the computation for all lists of "type" T and for all functions T -> R.

Of course, this computation is then abstracted (for use by others) simply into:

    Map(list, f) ≜ [i ∈ DOMAIN list ↦ f[list[i]]]

which is how you'd normally write this in TLA+. This definition is fully polymorphic, as it's an operator, not a function. If we wanted a function instead, we need "type parameters":

    CONSTANTS T, R
    map[list ∈ Seq(T), f ∈ [T → R]] ≜ [i ∈ DOMAIN list ↦ f[list[i]]]

which is a proper higher-order function (but these functions are proper functions, not "functions" or computations).

In any event, f here is a function, not a computation. If for some reason you want to actually use a computation, you would need to specify more precisely what your expectations are of that computation (e.g., that it can take an argument at all). But, again, that's not how it's normally done in TLA+.

[1]: See here https://pron.github.io/posts/tlaplus_part3#plotkins-parallel... or here https://www.youtube.com/watch?v=15uy9Ga-14I

> In any event, f here is a function, not a computation. If for some reason you want to actually use a computation

Yes, absolutely I want to use a computation! The point is that I want to understand how TLA+ can abstract over computations.

First, take a look at the parallel or example [1]. It's a computation that manipulates two other completely arbitrary ones, in a simple, compositional way that's not possible in any other formalism I'm aware of. The idea is not too different from how continuous dynamical systems are composed to describe "higher order" systems, despite first-order representation.

Doing a "map" of a completely arbitrary computation f, would look like this:

    CONSTANTS T (* the "type" of elements in the in/out list *)
    VARIABLES in, out, f_param, f_result, f_done

    Map ≜ ∧ in ∈ Seq(T)
          ∧ f_param = Head(in)
          ∧ □[∧ f_done = TRUE ∧ f_done' = FALSE (* wait for f to work *)
              ∧ out'     = Append(out, f_result])
              ∧ f_param' = Head(in)               (* send another element to f *)
              ∧ in'      = Tail(in)
              ∧ UNCHANGED f_result
             ]_⟨f_param, in, out⟩ (* we don't allow f to change f_param, in or out *)

and then, the composition or the "application" would be:

    Map ∧ f

Nothing here guarantees that the computation f does any of those and that it terminates. We could do that by adding an assumption about f's behavior, that states that f behaves like a subroutine:

    f ⇒ □(f_done = FALSE ↝ f_done = TRUE)

which states that if ever f_done is false, f will cause it to eventually become true.

This is similar to how ODEs and processes in process calculi are composed, and all of this can be abstracted nicely into a "subroutine call" operator as I do in part 4. It is more cumbersome than sequential formalisms as composition is parallel "by default", but the technique is never used in practice precisely because of the Boolean algebra of computation that allows you to abstract appropriate computations as functions.

[1]: This is the exact spot in the video: https://youtu.be/15uy9Ga-14I?t=37m34s

Thanks. It will take me some time to digest this.

My 40 minute talk is a good intro to the theory, and the posts cover everything in great detail.

Also, I've given it some more thought, and I think that my original (slightly corrected) answer is actually the better way (even when dealing with computation), and I'll explain why below:

    CONSTANTS T, R (* the "type" of elements in the in/out list *)
    VARIABLES in, out, f

    Map ≜ ∧ in ∈ Seq(T)
          ∧ f ∈ [T → R]
          ∧ □[∧ Len(in) > 0
              ∧ out' = Append(out, f[Head(in)])
              ∧ in' = Tail(in)
              ∧ UNCHANGED f]_⟨f, in, out⟩

Now, I too fell victim to the Whorfian syndrome, and thought in terms of functions (subroutines), instead of thinking about the meaning of the map program. What does a map program mean? I.e., in the semantics of TLA, a program is the set of all its possible executions. Every parameter, is just another dimension of nondeterminism, which adds more possible execution. This holds for ordinary value parameters, but also for "function" arguments. What do we know about the function argument? Well, that it behaves like a partial function, meaning it could either never terminate, or return a response (which map will then write to the output list), but we also know (or, rather, choose to assume) that the argument isn't an arbitrary computation, but a pure "functions", which means that for every input it must return the same output. The above specification says exactly that (it may not terminate because we haven't added liveness conditions).

Map can then be composed with another computation that implements the mapping, and, if you watch the talk you'll see that the other computation may take as many steps as it likes due to stuttering invariance. The f function merely encodes our assumption about the mapping computation's behavior, namely that it always yields the same output to the same input. Without this assumption, the specification will simply look like:

    CONSTANTS T, R (* the "type" of elements in the in/out list *)
    VARIABLES in, out

    Map ≜ ∧ in ∈ Seq(T)
          ∧ □[∧ Len(in) > 0 (* sorry, forgot this before; must stop when the list is empty *)
              ∧ out' = ∃ y ∈ R : Append(out, y) (* completely nondeterministic in R *)
              ∧ in' = Tail(in)]_⟨f, in, out⟩

Now, we just state that any other computation must yield a value in R, but may not be "pure" and so may yield different values for the same input.

I may add this with the explanation to the posts.