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