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