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.
Well, interested intellectually, but yes, I'm an engineer and I judge the utility of tools by their applicability to the work of engineers. That a tool like Coq could theoretically be used to fully reason about and verify a large program is of little interest to me, as no one so far has been able to do that, let alone enable engineers to do that.
BTW, I'm not too sure what the point on SMT was. SMT just uses SAT for whatever theory is needed (and possible). TLA+ uses SMT (as well as Isabelle) extensively as automated tactics in deductive proofs (in set theory), which I have only just started to use. SMTs (and certainly SATs) are not related in any way to one mathematical formulation or another, just like garbage collection isn't. In fact, SATs are commonly used today in bounded temporal-logic model checking.
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 ...?
> Maybe translation of specification into implementation is always the easy part, though ...?
Not only is it the easy part, but we're talking about reasoning about programs. If reasoning requires end-to-end certification you're working too hard.
Even within TLA+, you don't work at one refinement level. The lowest level is just too low, and therefore too hard for some proofs. You create a couple of sound refinements -- simpler state machines that capture the relevant essence -- and verify the behavior of yours. It's simpler than it sounds (refinement is just plain old logical implication, =>, in TLA) but it does take effort to reason about -- let alone prove -- a complex algorithm regardless of the formalism you use. FP doesn't make it easier, and it does require more difficult math.
> 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.
> > 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...
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.