[lmm]

> That's the whole point in thinking of algorithms, not of code. I'd guess that this is what you do anyway -- regardless of the language. You don't necessarily always reach the same level -- e.g. once your complex distributed blockchain needs to find the maximal number in a list, you may go down to the index level in an imperative language, yet stop at the fold level in FP, and that's fine (you decide what an abstract machine can do at each step) -- but ultimately, at some point, you always think of your algorithm in the abstract -- you see it running in your mind -- rather than in linguistic terms, and that is the interesting level to reason about it. Forget about FSMs. What you imagine is pretty much the abstract state machine you can reason about mathematically.

This is a fascinating view, but no, I really don't. I think of the function that finds the maximal number in a list as a mathematical function (that is, "really" a set of pairs - a giant lookup table, that the implementing computer will have some tricks for storing in a finite amount of memory but those tricks are implementation details). I think of a function composed of two functions (when I think about it at all) as a bigger table (like matrix multiplication) - not as anything stateful, and not as anything involving steps. Like, if I think about 5 + (2 * 3), I think of that as 5 + 6 or 11, and sure you can model that as a succession of states if you want but I don't find that a helpful/valuable way to think about it. It seems like you want to think of the process of evaluation as first-class, when as far as I'm concerned it's an implementation detail; I see my program as more like a compressed representation of a lookup table than a set of operations to be performed.

[pron]

> I think of the function that finds the maximal number in a list as a mathematical function

My point is not how you would classify the object which is the program, but how you would go about programming it. You can think of it as a lookup table all you want, but you will define your algorithm as some state machine. Maybe looking for the maximum value is too simple, as the use of a combinator is too trivial, but think of a program that sorts a list. You can imagine the program to be a function if you like, but when you design the algorithm, there is no way, no how, that you don't design it as a series of steps.

> not as anything stateful

Again, don't conflate what programmers normally think of as "stateful" with the concept of a state in an abstract state machine.

> and sure you can model that as a succession of states if you want but I don't find that a helpful/valuable way to think about it.

I don't find it helpful, either, so I don't do it (more on that later). Whether you want to say that 5 + (2 * 3) in TLA is one step or several is completely up to you. TLA is not a particular state machine model like lambda calculus or a Turing machine, but an abstract state machine.

> It seems like you want to think of the process of evaluation as first-class, when as far as I'm concerned it's an implementation detail

You are -- and I don't blame you, it's hard to shake away -- thinking in terms of a language, which has a given syntax and a given semantics and "implementation". When reasoning about algorithms mathematically, there are no "implementation" details, only the level of the algorithm you care to specify. In TLA+ you can define higher-order recursive operators like "reduce" that does a reduction in one step -- or zero-time if you like -- or you can choose to do so over multiple steps. It is up to you. There is no language, only an algorithm, so no "implementation", only the level of detail that interests you in order to reason about the algorithm. Personally, for simple folds I just use the reduce operator in "zero-time", because I really don't care about how it's done in the context of my distributed data store. But if you wanted to reason about, say, performance of a left-fold or a right-fold, you'll want to reason about how they do it, and how any computation is done is with a state machine.

[lmm]

> You can think of it as a lookup table all you want, but you will define your algorithm as some state machine. Maybe looking for the maximum value is too simple, as the use of a combinator is too trivial, but think of a program that sorts a list. You can imagine the program to be a function if you like, but when you design the algorithm, there is no way, no how, that you don't design it as a series of steps.

Again, disagree. I think of it more as defining what a sorted list is to the computer. (An extreme example would be doing it in Prolog or the like, where you just tell the computer what it can do and what you want the result to look like). It's very natural to write mergesort or bubblesort thinking of it a lookup table - "empty list goes to this, one-element list goes to this, more-than-one-element list goes to... hmm, this".

Now that's not an approach that's ever going to yield quicksort, but if we're concerned with correctness and not so much about performance then it's a very usable and natural approach.

> You are -- and I don't blame you, it's hard to shake away -- thinking in terms of a language, which has a given syntax and a given semantics and "implementation". When reasoning about algorithms mathematically, there are no "implementation" details, only the level of the algorithm you care to specify. In TLA+ you can define higher-order recursive operators like "reduce" that does a reduction in one step -- or zero-time if you like -- or you can choose to do so over multiple steps. It is up to you. There is no language, only an algorithm, so no "implementation", only the level of detail that interests you in order to reason about the algorithm.

I think you're begging the question. If you want to reason about an algorithm - a sequence of steps - then of course you want to reason about it as a sequence of steps. What I'm saying is it's reasonable and valuable, under many circumstances, to just reason about a function as a function. If we were doing mathematics - actual pure mathematics - it would be entirely normal to completely elide the distinction between 5 + (2 * 3) and 11, or between the derivative of f(x) = x^2 and g(x) = 2x. There are of course cases where the performance is important and we need to include those details - but there are many cases where it isn't.

> if you wanted to reason about, say, performance of a left-fold or a right-fold, you'll want to reason about how they do it, and how any computation is done is with a state machine.

Sure. (I think/hope we will eventually be able to find a better representation than thinking about it as a state machine directly - but I completely agree that the functional approach simply doesn't have any way of answering this kind of question at the moment).

[pron]

> Again, disagree. I think of it more as defining what a sorted list is to the computer. (An extreme example would be doing it in Prolog or the like, where you just tell the computer what it can do and what you want the result to look like).

Exactly, but the point is defining at what level. Take your Prolog example. This is how you can define what a sorted list is in TLA+:

    IsSorted(seq) ≜ ∀i,j ∈ 1..Len(seq) : i < j => seq[i] ≤ seq[j]
    Sorted(seq) ≜ CHOOSE res ∈ Perms(seq) : IsSorted(s)

So this is a definition, but it's not an algorithm. Yet, in TLA+ it could describe a state machine of sorts: the nondeterministic state machine that somehow yields a sorted list. Any particular sorting algorithm is a refinement of that machine. Of course, the refinement does not need to happen in one step. You can describe a mergesort as a machine that somehow merges, which is a refinement of the magical sorting machine. Any machine that merges, say, using a work area in a separate array, is then a refinement of that. You decide when to stop.

If there's a difference in how you "define" a sorted list via bubble-sort or mergesort in your lookup table image that difference is an abstract state machine. For example, in the mergesort case your composition "arrows" are merges. You have just described a (nondeterministic) state machine. Otherwise, if your lookup table algorithm doesn't have any steps, it must simply map the unsorted array to the sorted array and that's that. If there is any intermediate mappings, those are your transitions.

The state machines are nondeterministic, so you don't need to say "do this then do that". It's more like "this can become that through some transformation". Every transformation arrow is a state transition. You don't need to say in which order they are followed.

Here is a certain refinement level of describing mergesort

    ∃x, y ∈ sortedSubarrays : x ≠ y ∧ x[2] + 1 = y[1]
                     ∧ array' = Merge(array, x, y) 
                     ∧ sortedSubarrays' = {sortedSubarrays \ {x,y}} ∪ {<<x[1], y[2]>>}

That's it; That's the state machine for mergesort (minus the initial condition). It is completely declarative, and it basically says "any two adjacent sorted subarrays may be merged". Note that I didn't specify anything about the order in which subarrays are sorted; this machine is nondeterministic. Even that may be too specific, because I specified that only one pair of subarrays picked at each step. I could have said that any number of pairs is picked, and then my specification would be a refinement of that.

You can define an invariant:

   Inv ≜ [](∀x ∈ sortedSubarrays : IsSorted(x))

The box operator [] means "always". Then you can check that

    MergeSort => Inv

to assert that the sorted subarrays are indeed all sorted.

> I think/hope we will eventually be able to find a better representation than thinking about it as a state machine directly

There are two requirements: first, the formulation must be able to describe anything we consider an algorithm. Second, the formulation must allow refinement, i.e. the ability to say that a mergesort is an instance of a nondeterministic magical sorting algorithm, and that a sequential or a parallel mergesort are both instances of some nondeterministic mergesort.

[lmm]

> If there's a difference in how you "define" a sorted list via bubble-sort or mergesort in your lookup table image that difference is an abstract state machine.

Perhaps. But very often that's precisely the kind of difference I want to elide, since the two are equivalent for the purposes of verifying correctness of a wider program that uses one or the other.

I find it a lot more difficult to think about a state machine than about a function. What is it I'm supposed to be gaining (in terms of verifying correctness) by doing so? (I might accept that certain aspects of program behaviour can only be modeled that way - but certainly it's usually possible to model a large proportion of a given program's behaviour as pure functions, and I find pure functions easier to think about by enough that I would prefer to divide my program into those pieces so that I can think mostly about functions and only a little about states).

[pron]

I think we're talking at two different levels here. I am not talking about using a sorting routine in a program, but about writing a sorting routine. You want to know that your sorting routine actually sorts. Your routine is a state machine; its blackbox description is a function. You want to prove that your state machine implements the function. Our goal is to verify that mergesort actually sorts. Not that the air traffic control program using mergesort works (we could, but then the ATC program would be the state machine, and sorting would be just a function).

> Perhaps. But very often that's precisely the kind of difference I want to elide, since the two are equivalent for the purposes of verifying correctness of a wider program that uses one or the other.

This means that both are refinements of the "magical sorting machine". You can use "magical sorting" in another TLA+ spec, or, as in this running example, prove that mergesort is a refinement of "magical sorting". If what you want to specify isn't a mergesort program but an ATC program that uses sorting, of course you'd use "magical sorting" in TLA+. You specify the "what" of the details you don't care about, and the "how" of the details you do.

> I find it a lot more difficult to think about a state machine than about a function.

Sure, but again when you want to verify an algorithm, it may use lots of black boxes, but the algorithm you are actually verifying is a white box. That algorithm is not a function; if it were, then you're not verifying the how just stating the what. The how of whatever it is that you actually want to verify (not the black boxes you're using) is a state machine. Other ways of thinking about it include, say, process calculi, lambda calculus etc., but at the point of verifying that, considering it a function is the one thing you cannot do, because that would be assuming what you're trying to prove.

[lmm]

> Sure, but again when you want to verify an algorithm, it may use lots of black boxes, but the algorithm you are actually verifying is a white box. That algorithm is not a function; if it were, then you're not verifying the how just stating the what. The how of whatever it is that you actually want to verify (not the black boxes you're using) is a state machine. Other ways of thinking about it include, say, process calculi, lambda calculus etc., but at the point of verifying that, considering it a function is the one thing you cannot do, because that would be assuming what you're trying to prove.

Well a function is necessarily a function (if we enforce purity and totality at the language level). Presumably what we want to verify is that its output has certain properties, or that certain relations between input and output hold. But that seems like very much the kind of thing we can approach in the same way we'd analyse a mathematical function.

[pron]

Let me also address this with some snarky quotes by Lamport[1] (and just add, that having tried what he suggests on real-world programs, although what he says may sound more complicated, it is actually simple):

> Computer scientists collectively suffer from what I call the Whorfian syndrome — the confusion of language with reality

> [R]epresenting a program in even the simplest language as a state machine may be impossible for a computer scientist suffering from the Whorfian syndrome. Languages for describing computing devices often do not make explicit all components of the state. For example, simple programming languages provide no way to refer to the call stack, which is an important part of the state. For one afflicted by the Whorfian syndrome, a state component that has no name doesn’t exist. It is impossible to represent a program with procedures as a state machine if all mention of the call stack is forbidden. Whorfian-syndrome induced restrictions that make it impossible to represent a program as a state machine also lead to incompleteness in methods for reasoning about programs.

> To describe program X as a state machine, we must introduce a variable to represent the control state—part of the state not described by program variables, so to victims of the Whorfian syndrome it doesn’t exist. Let’s call that variable pc.

> Quite a number of formalisms have been proposed for specifying and verifying protocols such as Y. The ones that work in practice essentially describe a protocol as a state machine. Many of these formalisms are said to be mathematical, having words like algebra and calculus in their names. Because a proof that a protocol satisfies a specification is easily turned into a derivation of the protocol from the specification, it should be simple to derive Y from X in any of those formalisms. (A practical formalism will have no trouble handling such a simple example.) But in how many of them can this derivation be performed by substituting for pc in the actual specification of X? The answer is: very, very few.

> Despite what those who suffer from the Whorfian syndrome may believe, calling something mathematical does not confer upon it the power and simplicity of ordinary mathematics.

Obviously, we all suffer from the Whorfian syndrome, but I think it's worthwhile to try and shake it off. Luckily, doing it doesn't require any study -- just some thinking.

[1]: http://research.microsoft.com/en-us/um/people/lamport/pubs/d...