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