> I think it's safe to say that most mathematicians in 2016 -- let alone software engineers -- are pretty unfamiliar with category theory

I'm sure that's true for software engineers, but my experience is that category theory has permeated most fields to a significant degree. Many recent graduate-level texts on fields of mathematics from topology to differential geometry to algebra incorporate at least basic category theory like functors and natural transformations. It's even more common at the research level. And I say all of this not having actually met a single actual category theorist, only those in other fields who used at least some of it.

> Those systems are predicated on denotational semantics, which is a formalization that identifies a computation with the function it computes ... rather than view the computation as built up from functions

You know there's operational semantics too, right? Operational semantics typically describes the behaviour of your program as a state machine, especially the small step type of operational semantics.

> I was talking about FP there, and, I think, operational semantics must be embedded in FP.

I'm not sure what you mean. Are you claiming that operational semantics is somehow a poor fit for FP?

I was being vague and imprecise. Obviously, any semantics is semantics of a language, and every language has its own perfectly fine operational semantics. I think that FP is a non-optimal first-choice for operational reasoning; let's call it that.

But while I have your attention, let me try to put the finger on two concrete problem areas in the typed-PFP reasoning. Now, I'm not saying that this isn't useful for a programming language; I am saying that it is a poor choice for reasoning about programs. I think that FP has to discrete "jumps" between modes, that are simply unnecessary for reasoning and do nothing but complicate matters (again, they may be useful for other reasons):

The first is the jump between "plain" functional code and monadic code. Consider an algorithm that sorts list of numbers using mergesort. The program could be written to use simple recursion, or, it could be written using a monad, with the monadic function encoding just a single step. Those two programs are very different but they encode the very same algorithm! The first may use a more denotational reasoning, and the second a more operational one. In TLA, there is no such jarring break. You can specify an algorithm anywhere you want on a refinement spectrum. Each step may be just moving a single number in memory, splitting the array, all the way to sorting in one step. The relationship between all these different refinement levels is a simple implication:

  R1 => R2 => R3

where R3 may be completely denotational and not even algorithmic as in:

   done => result = Sorted(input)

(assuming some operator Sorted).

The second discrete jump is between the program itself and the types. I was just talking to an Agda-using type theorist today, and we noted how a type is really a nondeterministic program specifying all possible deterministic programs that can yield it. This is a refinement relation. Yet, in FP, types are distinct from programs (even in languages where they use the same syntax). In TLA the relationship between a "type", i.e. a proposition about a program and the program is, you guessed it, a simple refinement, i.e. simple logical implication (he figures that intermediate refinement steps are analogous to a "program with holes" in Agda). So, the following is a program that returns the maximal element in a list:

A2 ≜ done = FALSE ∧ max = 0 ∧ [](done' = TRUE ∧ max' = Max(input))

but it is also the type (assuming dependent types) of all programs that find the maximum element in a list, say (details ommitted):

A1 ≜ done = FALSE ∧ max = {} ∧ i = 0 ∧ [](IF i = Len(input) THEN done' = TRUE ELSE (input[i] > max => max' = input[i]) ∧ i' = i + 1)

Then, A1 => A2, because A1 is a refinement of A2.

So two very central concepts in typed-PFP, namely monads and types are artificial constructs that essentially just mean refinements. Not only is refinement a single concepts, it is a far simpler concept to learn than either monads or types. In fact, once you learn the single idea of an "action" in TLA, which is how state machines are encoded as logic (it is not trivial for beginners, but relatively easy to pick up), refinement is plain old familiar logical implication.

So I've just removed two complicated concepts and replaced it with a simple one that requires little more than highschool math, all without losing an iota of expressivity or proving power.

So how do you write the type "forall a. a -> a -> a" in TLA?

That depends what it is that you want to specify: a function or a computation (i.e., a machine). In TLA+ as in "reality" computations are not functions, and functions are not computations.

We'll start with a function. It's basically `[a -> [a -> a]]` or `[a × a -> a]`. More completely (to show that `a` is abstract):

    CONSTANT a, f
    ASSUME f ∈ [a -> [a -> a]]

`CONSTANT` means that a can be anything (formally, any set)

If you want to specify a computation, that, when terminates[1] returns a result in `a`, the "type" would be `[](done => result ∈ a)` (where [] stands for the box operator, signifying "always"), or more fully:

    CONSTANT a, Input
    ASSUME Input ∈ a × a
    VARIABLES done, result
    f ≜ ... \* the specification of the computation
    THEOREM f => [](done => result ∈ a)

So the first type is purely static. A set membership. The second has a modality, which says that whenever (i.e., at any step) `done` is true, then `result` must be in `a`.

------

[1]: Let's say that we define termination as setting the variable `done` to TRUE. BTW, in TLA as in other similar formalisms, a terminating computation is a special case of a non-terminating one, one that at some finite time stutters forever, i.e., doesn't change state, or, formally <>[](x' = x), or the sugared <>[](UNCHANGED x) namely eventually x is always the same (<> stands for diamond and [] for box; for some reason HN doesn't display those characters)

Actually, I've thought of something that will be an even better example. You mentioned "reduce" here

https://news.ycombinator.com/item?id=11910858

Could you link to its implementation?

I'll quote my own:

    Reduce(Op(_, _), x, seq) ==
        LET RECURSIVE Helper(_, _)
        Helper(i, y) ==
            IF i > Len(seq) THEN y
                            ELSE Helper(i + 1, Op(y, seq[i]))
        IN Helper(1, x)

A couple of things. First, the need for the helper is just a limitation of the language that doesn't allow recursive operators to take operators as arguments. Second, I used indexing, but you can use the Head and Tail operators. It's just that I use this often, and I care about the model-checking performance. Finally, Reduce is an operator not a function (it is not a function in the theory). Hence, its domain (for all arguments that aren't operators) is "all sets" something that would be illegal as a "proper" function (Russel's paradox). Operators, like functions, can be higher order, but they're not "first-class", i.e., they can't be considered "data". Functions require a proper domain (a set).

> I'll quote my own: ...

Thanks

> Operators, like functions, can be higher order, but they're not "first-class", i.e., they can't be considered "data".

Do you mean you can't pass an operator to a function (or make it the argument of a computation)?

EDIT: Or more generally, what are the consequences of it not being "first-class", i.e., not being considered "data"?

> Do you mean you can't pass an operator to a function

Right. Functions are objects in the theory, and must have a domain which is a set. Operators are outside the theory, and aren't in any sets. You also can't return an operator as a result of an operator.

A function can, of course, return a function, but functions can't be polymorphic within a single specification. So they must have a particular (though perhaps unspecified) set as their domain. Why? Because there is no such thing as polymorphic functions in math. Polymorphism is a feature of a certain language or "calculus", and TLA+ is about algorithms, not about a specific linguistic representation of them. "Polymorphism" of the kind I've shown does make sense, because you determine the level of the specification, and you can say that you want to reason about the use of a function (or a computation) without assuming anything more specific other than your explicit assumptions about a certain set. But that is not to say that you can’t have an operator that “creates” functions generically. E.g.:

    Foo(a) ≜ [x ∈ a × a ↦ x[1]]   /or/  Foo(a) ≜ LET f[x ∈ a × a] ≜ x[1] IN f

Which you can then use like so: Foo(Nat)[1, 2]. Foo must be an operator because its argument `a` ranges over all sets, so it's not a proper domain (Russel, etc.)

> or make it the argument of a computation

Ah, that actually you can do, and it's quite common as it's very useful. A constant can be an operator (a variable can't because a variable is state, and state must be an object in the theory). For example, it's useful for taking a relation as input (although a relation can also be defined as a set of pairs, so it’s an object in the theory). If in the polymorphic example you want to say that the set `a` is partially ordered (because you're specifying a sorting algorithm), you can write[1]:

    CONSTANTS a, _ ⊑ _
    ASSUME ∀x, y, z ∈ a :
              ∧ x ⊑ x
              ∧ x ⊑ y ∧ y ⊑ x => x = y
              ∧ x ⊑ y ∧ y ⊑ z => x ⊑ z

All of this, BTW, is actually the "+" in TLA+ (which is a bit technical, and trips me up occasionally), and not where the core concepts lie, which is the TLA part. Lamport would say you’re focusing on the boring algebraic stuff, rather than the interesting algorithmic stuff… I guess you could come up with another TLA language, with a different "+", but the choice of this particular "+" (i.e, set theory) was made after experimentation and work with engineers back in the '90s (Lamport says that early versions were typed). There is actually a type inferencer for TLA+, which is used when proofs are passed to the Isabelle backend (or intended to be used, I don't know; the proof system is under constant development at INRIA). So you get rich mathematical reasoning using simple math — no monads or dependent types (nor any types) necessary. Those things can be useful (for automatic code extraction, maybe, or for deep mathematical theories of languages — not algorithms), but for mathematically reasoning about programs, this is really all you need. And it works well, in the industry, for programs as small as a sorting routine or as large as a complex distributed database.

[1]: The aligned conjunctions are a syntactic convenience to avoid parentheses.

Are those actually polymorphic? It seems like you've assumed a specific, concrete, a.

EDIT: On a second look, "CONSTANT" seems more like declaring a variable than requiring a concrete type.

EDIT 2: Hmm, still not completely sure about this ...

Constants are external inputs to a specification. All you know about them is what you assert in the assumptions. When you use the proof system, the assumptions are your axioms and if you don't have any, then it's really polymorphic. If you use the model checker, you'll need to supply the checker with a concrete -- and finite[1] -- set for all constants.

[1]: The one supplied with TLA+, called TLC, is powerful enough to model-check an expressive language like TLA+, but it's algorithm is rather primitive; it's an "old-school" explicit state model-checker. A more modern, state-of-the-art model checker is under research: http://forsyte.at/research/apalache/. BTW, modern model checkers are amazing. Some can even check infinite models.

You always want to decompose your model to help reasoning about it though, no? Even if you're modeling as a state machine, rather than a single big state machine you'd want to separate it into small orthogonal state machines as much as possible.

I see the functional approach as taking that one step further: separate the large proportion of the program that doesn't depend on state at all (i.e. that's conceptually just a great big lookup table - which is the mathematical definition of a function) from the operations that fundamentally interact with state. I find anything involving state machines horrible to reason about, so I'd prefer to minimize the amount of the program where I have to think about them at all.

> 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.

> 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.

> 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).

> 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.

> 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).

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.

> 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.

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...

I feel like you have confused quite a few concepts here.

First, type theory based proof assistants (like Coq) and model checkers are very different tools with very different guarantees. Most model checkers are used for proving properties about finite models and can not reason about infinite structures.

A type theory with inductive types gives one a mechanism for constructing inductive structures, and the ability to write proofs about them.

I am not sure how you have equated denotational semantics and type theory but there is no inherent connection, denotational semantics are just one way to give a language semantics. One can use them to describe the computational behavior of your type theory, but they are not fundamental.

Category theory and type theory have a cool isomorphism between them, but otherwise can be completely silo'd you can be quite proficient in type theory and never touch or understand any category theory at all.

On the subject of TLA+, Leslie Lamport loves to talk about "ordinary mathematics" but he just chose a different foundational mathematics to build his tool with, type theory is an alternative formulation in this regard. One that is superior in some ways since the language for proof, and programming is one and the same and does not require strange stratification or layering of specification and implementation languages.

Another issue with many of these model based tools is the so called "formality gap" building a clean model of your program and then proving properties is nice, but without a connection to your implementation the exercise has questionable value. Sure, with distributed systems for example, writing out a model of your protocol can help find design bugs, but it will not stop you from incorrectly implementing said protocol. In the distributed systems even with testing, finding safety violations in practice is hard, and many of them can occur silently.

Proof assistants like Coq make doing this easier since your implementation and proof live side by side, and you can reason directly about your implementation instead of a model. If you don't like dependently typed functional languages you can check out tools like Dafny which provide a similar work style, but with more automation and imperative programming constructs.

> This formulation serves as the basis for most formal reasoning of computer programs.

On this statement I'm not sure what community you come from, but much of the work going on in the research community is using things like SMT which exposes SAT and a flavor of first order logic, an HOL based system like Isabelle, or type theory, very few people use tools like set theory to reason about programs.

> Engineers, however, already have nearly all the math they need to reason about programs and algorithm in the common mathematical way (they just may not know it, which is why I so obnoxiously bring it up whenever I can, to offset the notion that is way overrepresented here on HN that believes that "PFP is the way to mathematically reason about programs".

Finally this statement is just plain not true, abstractly its easy to hand way on paper about the correctness of your algorithm. I encourage you to show me the average engineer who can pick up a program and prove non-trivial properties about its implementation, even on paper. I wager even proving the implementation of merge sort correct would prove too much. I've spent the last year implementing real, low-level systems using type theory, and this stuff is hard if you can show me a silver bullet I would be ecstatic, but any approach with as much power and flexibility is at least as hard to use.

Its not that "PFP" (and its not PFP, its type theory that makes this possible) is the "right way" to reason about programs but that it makes it possible to reason about programs. For example, how do you prove a loop invariant in Python? how would you even start? I know of a few ways to do this, but most provide a weaker guarantee then you would type theory version would, and requires a large trusted computing base.

> > This formulation serves as the basis for most formal reasoning of computer programs.

> On this statement I'm not sure what community you come from, but much of the work going on in the research community is using things like SMT which exposes SAT and a flavor of first order logic, an HOL based system like Isabelle, or type theory, very few people use tools like set theory to reason about programs.

Pron is an engineer and he cares about what's easy for engineers to use. He's uninterested in research.

Compcert doesn't qualify as a large program?

No. It's medium-sized; and it required a world expert, and it required a lot of effort, and even he had to skip on the termination proofs because they proved too hard/time-consuming, so he just put in a counter and throws a runtime exception if it runs out.

> building a clean model of your program and then proving properties is nice, but without a connection to your implementation the exercise has questionable value

This is one thing that has always confused me about TLA+ since pron introduced me to it. Maybe translation of specification into implementation is always the easy part, though ...?

> > I encourage you to show me the average engineer who can pick up a program and prove non-trivial properties about its implementation, even on paper.

> I'm one.

This doesn't seem right. TLA helps you prove properties of its specification, not its implementation. Or are you saying you can somehow prove properties of implementation too?

> I wager that I can take any college-graduate developer, teach them TLA+ for less than a week, and then they'd prove merge-sort all by themselves.

Sure, but prove properties of its specification, not its implementation. Unless I'm missing something ...

> State machine and temporal logic approaches have made it possible to reason about programs so much so that thousands of engineers reason about thousands of safety-critical programs with them every year.

Again, surely the specification of programs not their implementation?

> > For example, how do you prove a loop invariant in Python?

> ... Sure, there may be a bug in the tranlation to Python

Absolutely. That's the whole point. Translating it to Python is going to be hard and full of mistakes.

> but we're talking about reasoning not end-to-end certification, which is beyond the reach -- or the needs -- of 99.99% of the industry

If the implementation part truly is (relatively) trivial then this is astonishingly eye opening to me. In fact I'd say it captures the entire essence of our disagreements over the past several months.

> The easiest way to reason about a Python program is to learn about state machines, and, if you want, use a tool like TLA+ to help you and check your work.

No, that's the "easiest way" of reasoning about an algorithm that you might try to implement in Python.

> TLA helps you prove properties of its specification, not its implementation. Or are you saying you can somehow prove properties of implementation too?

What do you mean by "implementation"? Code that would get compiled to machine code? Then no. But if you mean an algorithm specified to as low a level as that provided by your choice of PL (be it Haskell or assembly), which can then be trivially translated to code, then absolutely yes. In fact, research groups have built tools that automatically translate C or Java to TLA+, preserving all semantics (although, I'm sure the result is ugly and probably not human-readable, but it could be used to test refinement).

Usually, though, you really don't want to do that because that's just too much effort, and you'd rather stop at whatever reasonable level "above" the code you think is sufficient to give you confidence in your program, and then the translation may not be trivial for a machine, but straightforward for a human.

> Translating it to Python is going to be hard and full of mistakes.

Not hard. You can specify the program in TLA+ at "Python level" if you like. Usually it's not worth the effort. Now, the key is this: full of mistakes -- sure, but what kind of mistakes? Those would be mistakes that are easy for your development pipeline to catch -- tests, types whatever -- and cheap to fix. The hard, expensive bugs don't exist at this level but at a level above it (some hard to catch bugs may exist at a level below it -- the compiler, the OS, the hardware -- but no language alone would help you there.

But I can ask you the opposite question: has there ever been a language that can be compiled to machine code, yet feasibly allow you to reason about programs as easily and powerfully as TLA+ does? The answer to that is a clear no. Programming languages with that kind of power have, at least to date, required immense efforts (with the assistance of experts), so much so that only relatively small programs have ever been written in them, and at great expense.

So it's not really like PFP is a viable alternative reasoning to TLA and similar approaches. Either the reasoning is far too weak (yet good enough for many purposes, just not uncovering algorithmic bugs) or the effort is far too great. Currently, there is no affordable way to reason with PFP at all.

> No, that's the "easiest way" of reasoning about an algorithm that you might try to implement in Python.

You specify until the translation is straightforward. If you think there could be subtle bugs in the translation, you specify further. I'm in the process of translating a large TLA+ specification to Java. There's a lot of detail to fill in that I chose not to specify, but it's just grunt work at this point. Obviously, if a program is so simple that you can fully reason about it in your head with no fear of subtle design bugs, you don't need to specify anything at all...