[pron]

Concrete imperative steps are extremely mathematical -- even elegantly so -- and most of software verification is predicated on this idea. Just like you can describe physics pretty precisely with simple math, you can do it with computation. The math of PFP is one particular approximation, chosen for its supposed utility as the basis for a language. It is more linguistic math than descriptive math. I also hope people adopt abstract mathematical thought when reasoning about their programs, but that has little to do with the kind of math they choose to model their programs' source code with.

[johncolanduoni]

Sure, you can model imperative steps in a variety of ways using mathematics, but for 99% of mathematics there is a far more direct link to pure functions. In how many branches of mathematics do you see a function that is anything but a mapping between sets (or types, or objects in a category). In terms of using the same kind of processes and intuitions, pure functional programming is much closer to mathematics as done by humans than imperative programming. Even theoretical computer science looks this way outside of particular algorithms being studied.

Not that this is some sort of indictment of imperative programming; it's a much better fit for a lot of different situations. But if you're trying to model something in abstract mathematics, pure or pure-ish function programming is likely to be a better solution. For example, look at the various proof assistants like Coq. Many of them are written in functional languages, and if you look at the code you can see why: the manipulation of formulas and proofs fits very well with an immutable, functional approach.

[pron]

> but for 99% of mathematics there is a far more direct link to pure functions.

But state transitions are pure! Deterministic state machines are nothing more than mathematical functions from one algorithm state to the next, and nondeterministic ones are binary relations! (see this for an overview: http://research.microsoft.com/en-us/um/people/lamport/pubs/s...) Those can then be mathematically manipulated, substituted and what-have-you elegantly and simply. This is how formal verification has been reasoning about programs since the seventies (early on the formalization was a bit more cumbersome, but the concept was as simple).

> For example, look at the various proof assistants like Coq.

For example, look at the specification language (and proof assistant) TLA+. It is far simpler than Coq, just as pure, and requires no more than highschool math.

Coq and other PFP formalizations are built on the core idea of denotational semantics, an approximation which at times only complicates the very simple math of computation, requiring exotic math like category theory.

> the manipulation of formulas and proofs fits very well with an immutable, functional approach.

The manipulation of formulas and proofs fits very well with the imperative approach, only no category theory is required, and core concepts such as simulation/trace-inclusion arise naturally without need for complex embeddings. "PFP math" is what arises after you've decided to use denotational semantics. The most important thing is not to confuse language -- for which PFP has an elegant albeit arcane mathematical formalization -- with the very simple mathematical concepts underlying computation.

PFP is an attempt to apply one specific mathematical formulation to programming languages (other similar, though perhaps less successful attempts are the various process calculi). But it is by no means the natural mathematics of computation. Conflating language with algorithms is a form of deconstructionism: an interesting philosophical concept, but by no means a simple one, and perhaps not the most appropriate one for a science. Short of that, we have the basic, simple core math, and on top of it languages, some espousing various mathematical formalizations, related to the core math in interesting ways, and some less mathematical. But the math of computation isn't created by the language!

[johncolanduoni]

> But state transitions are pure! Deterministic state machines are nothing more than (obviously, "pure") functions from one program state to the next, and nondeterministic ones are binary relations!

Okay, yes, but 99% of mathematics isn't deterministic state machines. So again, pure functions can model a lot of things, but deterministic state machines are foreign to the way people think about mathematics in most instances.

> For example, look at the pure specification language (and proof assistant) TLA+. It is far simpler than Coq, just as pure, and requires no more than highschool math.

Okay, that's completely fine as an example. I just mentioned Coq because it's one of the better known ones.

> Coq and other PFP formalizations are built on the core idea of denotational semantics, an approximation which at times only complicates the very simple math of computation, requiring exotic math like category theory.

I'm not sure where CiC (or any of the other recent type theories, including HOTT) requires category theory (which is hardly exotic in 2016). People who are doing meta-mathematics on these systems are interested in categorical models and such, but implementing and using these systems requires no category theory.

Categories are not fundamental objects in these theories; you have to build them just like you do in material set theories, although some parts of that process are easier (especially in HOTT). But that is the reverse of the link that you're claiming.

> The manipulation of formulas and proofs fits very well with the imperative approach, only no category theory is required, and core concepts such as simulation/trace-inclusion arise naturally without need for complex embeddings.

Again, no category theory is required (though I'm still not sure why this is a bad thing?) to develop a prover like Coq or TLA+. If you're bringing simulation and trace-inclusion into this, then you're just saying the stateful, imperative approach is well adapted to working with stateful, imperative systems. I agree, but how exactly does that equate to that approach having any benefit whatsoever for formalizing the rest of mathematics?

[pron]

> Okay, yes, but 99% of mathematics isn't deterministic state machines. So again, pure functions can model a lot of things, but deterministic state machines are foreign to the way people think about mathematics in most instances.

Sorry, I wasn't clear. 99% of mathematics isn't Schrödinger's equation either, but Schrödinger's equation is still relatively simple math. State machines are simple math, but math isn't state machines. State machines are the concept that underlies computation, and simple math is used to reason about them.

> I just mentioned Coq because it's one of the better known ones.

... and one of the least used ones, at least where software is concerned. There's a reason for that: it's very hard (let alone for engineers) to reason about computer programs in Coq; it's much easier (and done by engineers) to reason about computer programs in TLA+ (or SPIN or B-Method or Alloy).

> which is hardly exotic in 2016

I think it's safe to say that most mathematicians in 2016 -- let alone software engineers -- are pretty unfamiliar with category theory, and have hardly heard of type theory. 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". It is just one way, not even the most common one, and certainly not the easiest one).

> but implementing and using these systems requires no category theory.

Right, but we're talking about foundational principles of computation. Those systems are predicated on denotational semantics, which is a formalization that identifies a computation with the function it computes (yes, some of those systems also have definitional equality, but still, denotational semantics is the core principle), rather than view the computation as built up from functions (in fact, this is precisely what monads do and why they're needed, as the basic denotational semantics fails to capture many important computations). This formalization isn't any better or worse (each could be defined in terms of the other), but it is more complicated, and is unnecessary to mathematically reason about programs. It does require CT concepts like monads to precisely denote certain computations.

> If you're bringing simulation and trace-inclusion into this, then you're just saying the stateful, imperative approach is well adapted to working with stateful, imperative systems.

There are no "imperative systems". Imperative/functional is a feature of the language used to describe a computation, not the computation itself (although, colloquially we say functional/imperative algorithms to refer to those algorithms that commonly arise when using the different linguistic approaches). The algorithm is always a state machine (assuming no textual deconstructionism) -- whether expressed in a language like Haskell or in a language like BASIC -- and that algorithm can be reasoned about with pretty basic math. And I am not talking about a "stateful" approach, but a basic mathematical approach based on state machines (a non-stateful pure functional program also ultimately defines a state machine).

> I agree, but how exactly does that equate to that approach having any benefit whatsoever for formalizing the rest of mathematics?

Oh, I wasn't talking about a new way to formalize the foundation of mathematics (which, I've been told, is the goal of type theory), nor do I think that a new foundation for math is required to mathematically reason about computation (just as it isn't necessary to reason about physics). I just pointed out that algorithms have a very elegant mathematical formulation in "simple" math, which is unrelated to PFP. This formulation serves as the basis for most formal reasoning of computer programs.

[johncolanduoni]

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

[tome]

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

[pron]

Of course. But I was talking about FP there, and, I think, operational semantics must be embedded in FP. In the state machine view, operational semantics are simply a refinement SM of the denotational semantic (which could be also specified as a nondeterministic SM)

[lmm]

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.

[pron]

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

Your notion of state is too specific for the theoretical meaning. Which function is executing in an FP computation is also state, as is the values of its arguments. Every software system is a single, possibly nondeterministic state machine. The decomposition you speak of is merely a decomposition of the state transition into various chunks (formulas). You can think of an abstract state machine as a single (pure) function -- just like a simple FP program -- except not a function from the input to the output, but a function from one state to the next (kinda like a state monad's monadic function, but expressed more naturally). One last complication is that it isn't quite a function but a relation, as you want to express the fact that your state machine may do one of several things in the next state, e.g. to describe different interleaving of threads, or even to model the user generating input.

Another thing you want to do is refinement and abstraction, i.e. specify your algorithm in different levels of detail (machines with more or fewer states) and show that the properties you want are preserved in the abstraction. Of course, you won't do that for something as simple as a sorting algorithm, but you also want to reason about large complex things, like an OS kernel or a distributed database.

So TLA simplifies things further by saying that the whole world is a single state machine, and your specifications are restricted views of that "world machine". This allows you to specify a clock with minute second hands, and another specification of a clock with just a minute hand, and then say that both are views of the same clock, with the first being just a more refined description of it than the first (this is a problem with multiple state machines, as one takes a step every second, and the other only every minute).

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

Again, what you consider state and the "abstract state" in abstract state machines are not quite the same. There is no such thing as a program that doesn't depend on state. Wherever there's a program, there's state. If you implement an algorithm that finds the maximum element in a list of numbers by a simple traversal in a PFP language and in an impure imperative language, the result would look very different, but the algorithm is the same, hence the state and the state transitions are identical.

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. A mathematical state machine is simply a description of your program's steps (and every program is composed of steps) at any level of detail.

[jroesch]

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.

[tome]

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

[tome]

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

[pron]

> First, type theory based proof assistants (like Coq) and model checkers are very different tools with very different guarantees.

I wasn't talking about model checkers but about mathematical specification languages. Some of them have proof assistants to help prove them, some have model checkers to help prove them, and some (like TLA+) have both. But the point is the formulation, not the proof tool.

> I am not sure how you have equated denotational semantics and type theory

No, I said FP is based on denotational semantics, and that reasoning about (typed) FP programs requires some type theory.

> but he just chose a different foundational mathematics to build his tool with

(When I speak of the math I'd rather refer to the logic TLA rather than the tool TLA+, but that doesn't matter). Obviously there is no objective, external way to classify mathematical theories as easy or hard. But that tool requires little more than highschool math, and it's been shown to be readily grasped by engineers with little training and almost no support. I think this qualifies as an objective evidence -- if not proof -- that it is, indeed, simpler, and the main reason why I encourage engineers to learn that first, and only later learn "FP math" if they wish.

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

That "easier" bit is theoretical. AFAIK, there has been only one non-trivial real-world program written in Coq, it was written by a world-expert, it took a lot of effort in spite of being quite small, and even he had difficulties, so he skipped on the termination proofs.

> very few people use tools like set theory to reason about programs.

Don't use set theory if you don't want -- though it is easier by the measure I gave above -- as that's just the "static" part of the program. I'm talking about the dynamic part and temporal logic(s). TLs are far more common when reasoning about programs in the industry than any FP approach. Or even other approaches that work on Kripke structures, such as abstract interpretation.

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

> I wager even proving the implementation of merge sort correct would prove too much.

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.

> I've spent the last year implementing real, low-level systems using type theory, and this stuff is hard

It is. But I've spent the past few months learning and then using TLA+ to specify and verify a >50KLOC, very complex distributed data structure, and Amazon engineers use TLA+ to reason about much larger AWS services every day. It's not end-to-end certified development, but reasoning and certified proof of implementation are two different things. State-machine reasoning is just easier, and it doesn't require the use of a special language. You can apply it to Python, to Java or to Haskell.

> but that it makes it possible to reason about programs

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.

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

Python is not a mathematical formulation. But proving a loop invariant in TLA+ is trivial. Sure, there may be a bug in the tranlation to Python, 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, and will probably stay there for the foreseeable future. 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.