I've started writing a blog post series about that, but the main difference is how you view an algorithm. The "Milner tradition" views an algorithm as a program in some programming language (Bob Harper even said, "an algorithm is a program"). That language has a syntax and a semantics, and a program is an algebraic composition of syntactic element, which you reason about syntactically using the equations of the algebra.
To Lamport, and algorithm is an abstract mathematical concept. A computation is discrete dynamical system (analogous to a continuous dynamical system), which is generated by a machine (an algorithm), which expressed mathematically in a simple, almost-ordinary-math way, almost exactly like dynamical systems are expressed as ordinary differential equations. Reasoning is done entirely semantically (the syntax of Lamport's formalism isn't a programming language, and its semantics are simple mathematical semantics -- again, like ODEs).
In the conversation with Meijer, Lamport explains that he believes that "linguistic reasoning" 1. requires far more complicated math ("weird, computer science math", like domain theory, category theory, type theory etc.) but, in his opinion, that math doesn't really make reasoning about the algorithm any easier.
All I can say personally is that I find Lamport's view to be a more natural fit with how I think of algorithms (this is entirely subjective), and that learning his formalism to the level where you can specify and reason about very large, very complex real-world systems takes a "plain" engineer maybe two weeks of self study, while learning the more PL-based approaches to reach that level would take a programmer years. This is pretty objective. I can also say that I occasionally see academic papers that describe how to express and reason about some simple properties (like worst-case complexity) in Coq, which would be almost trivial for a TLA+ practitioner, no more than a month after first laying eyes on TLA+. So for me, at least, the difference is a pragmatic one.
I'm not from the Milner tradition, but I disagree with your criticisms of that tradition.
I think the key difference between TLA+ et al and the Milner tradition is automation.
In the Milner tradition, the automation follows sort of systematically from a proper formulation. So if you find the "right" way of formulating worst-case complexity, you get a lot more than just a way to state and hopefully prove some particular property -- you also get a way of automatically inferring that property and a sort of systematic way of baking your results into compiler infrastructure. This insight is perhaps masked by the fact that you can also formulate arbitrary properties in arbitrary styles in a dependent type theory... so to put it another way, the evidence for the fact that ML type systems are well-designed is the unification algorithm, not the type checker.
The TLA+ (et al.) story about automation is mostly "model checkers and invariant generators". In other words, the "hard stuff" is typically exogenous to the specification system/language. I know you might claim that model checking is sufficient, but I have a lot of experience with that approach and I respectfully disagree -- in part because the Milner tradition has produced a lot of insights that are often baked into model checkers and invariant generators. But also because this approach has fundamental scaling issues and designing around those constraints requires much more skill than advertised.
So while it's true that the type theory tradition is more difficult to understand, it's also true (IMO) that if you get something "right" in that tradition, it's far more powerful than getting something "right" in the TLA+ tradition.
I wouldn't call it automation, but program extraction. You are absolutely correct about program extraction, but those benefits are currently theoretical, yet they come at a very real, very high cost. Lamport says that if those approaches would one day be affordable -- use them, by all means -- but that day is far in the future. It is not 100% related to dependent types (I think), as tools like Isabelle also support program extraction, but they don't have dependent types (instead, they express properties directly in logic).
> In other words, the "hard stuff" is typically exogenous to the specification system/language.
1. I don't think that's the hard stuff. It's some other hard stuff.
2. Even in the PL approach, that hard stuff is mostly theoretical today.
> the Milner tradition has produced a lot of insights that are often baked into model checkers and invariant generators
I don't know about that. You may be right, but I don't think that's the case. AFAIK, most of that work -- and its inspiration -- is done by people who work with programs and logic, and not PLT.
> But also because this approach has fundamental scaling issues and designing around those constraints requires much more skill than advertised.
That's true, but the deductive approaches currently suffer from much greater scaling issues. Even Xavier Leroy, who, AFAIK, is the only person who ever managed to do an end-to-end verification of a non-trivial real-world program in Coq, says that model checkers work on larger problems than manual deduction (not that it matters; both model checking and manual deduction can be done in either approach, using very similar algorithms).
> if you get something "right" in that tradition, it's far more powerful than getting something "right" in the TLA+ tradition.
I'm not entirely sure what you mean. Proving correctness is the same in both approaches. It's all just logic. The benefit of program extraction is currently theoretical. The benefit of end-to-end verification is real, but end-to-end verification is so costly, and can work on such small programs, that it's a very specialized activity, and one that is explicitly outside the scope of TLA+ (although end-to-end has been done in TLA+, too).
I don't think that anyone would disagree that if one day a programming language that can both be used to affordably reason about programs -- as affordably as TLA+ -- and could at the same time be compiled to efficient machine code, and perhaps also significantly assist with the programming process itself, that would be a great thing. But there's no such language on the horizon.
Don't get me wrong: the work done in PLT is ambitious and extremely important. But TLA+ is an affordable way to "just" reason about programs today. It works because it's undertaken a far simpler task. But a simple, useful solution to a hard problem that works is more important for practitioners, today, than a much bigger problem, with an unclear solution, that may work one day in the far future.
I guess "fighting" really is an appropriate word for what he's doing when he describes or-introduction as the "Act-Stupid"-rule in that composition paper.
His alternative or-composition rule looks strange to me, since given either A or B it is entirely subsumed by simple implication, but his rule still seems to need both..? Or am I missing something about his notation?
Section 6.3 also contains unsubstantiated claims about what is "popular among computer scientists" and what "many computer scientist" do or that they "denigrate the use of ordinary mathematics". I mean, this guy knows who he is talking about, why not call them out on the specifics? (He does reference one paper, and then attacks it by comparing it to a specification he worked on, which he does not reference.)
He's obviously way smarter than me, and I think I understand his general position, but it's hard to get at his arguments when he wraps them in some much hostility.
Personally I'm more interested and fascinated by the stuff going on in the Milner camp, so I'm obviously biased against him. But I do think the most fruitful approach is to have many people working in different directions and seeing what falls out, instead of trying to prove a priori that a research direction is useless.
> I guess "fighting" really is an appropriate word for what he's doing
Oh, that article is especially trollish, but there are articles like that in both camps.
> His alternative or-composition rule looks strange to me, since given either A or B it is entirely subsumed by simple implication, but his rule still seems to need both..?
It's not about "needing" both, but about how proofs are decomposed. Sometimes you need to prove `A ∨ B ⇒ C`; that's your proof goal. To do that, you prove `A ⇒ C` and `B ⇒ C`. That's all. If you look at basic texts about formal reasoning, they're full of such rules (see, e.g. https://en.wikipedia.org/wiki/Natural_deduction)
But from a pragmatic perspective, I think this is clear: if you want to formally reason about large, real-world programs today (especially if they're concurrent or distributed) "Lamport's" approach is the only affordable way to do it. It is also mathematically simple, very elegant and fun. Whatever you're interested in academically, it also covers the most important concepts anyway (refinement/abstraction relations, inductive invariance), and, in the end how you work and think is basically the same.
Doesn't Lamport give exactly the argument that motivates the Milner tradition in section 6.4 of that paper?
There is one case in which it’s worth doing the extra
work: when the computer does a lot of it for you.
[..]
In that case, the extra work introduced by decomposition
will be more than offset by the enormous benefit of using
model checking instead of human reasoning
That's not what he means in that quote. He means that the extra work of decomposition (which can be done in either approach) is worth it if it's easier to use automated methods for each component separately. Those automated methods work equally well in both approaches (in practice, though, there is a production-quality model checker for TLA+, but not any that I'm aware of for "academic" programming languages). So your quote is completely orthogonal, and in any event, it is not the motivation for the "Milner approach".
There are several motivations for the PL approach: 1. an executable can be extracted from the code -- i.e., it can be compiled to an efficient program, 2. they believe that reasoning with syntax is easier, and 3. high-level reasoning could potentially assist in writing parts the program automatically. Lamport completely disagrees with point 2, and as to point 1, he says that had a language that could both reason about programs affordably and be compiled efficiently existed that would be great, but currently this is not the case. So he believes that they're sacrificing the simplicity of reasoning in a major way for the goal of having both programming and reasoning done in the same language. He may agree that it's a worthy goal, but one that we're currently far from attaining. He's interested in things that work on real-life software today. He says that how you program and how you reason about programs should not necessarily be the same, and if making them the same makes either of them significantly more complicated than would be possible when keeping them separate, then we should keep them separate.
To Lamport, and algorithm is an abstract mathematical concept. A computation is discrete dynamical system (analogous to a continuous dynamical system), which is generated by a machine (an algorithm), which expressed mathematically in a simple, almost-ordinary-math way, almost exactly like dynamical systems are expressed as ordinary differential equations. Reasoning is done entirely semantically (the syntax of Lamport's formalism isn't a programming language, and its semantics are simple mathematical semantics -- again, like ODEs).
Lamport's approach is best explained in the link I posted above (which is a very interesting read) and in section 6.3 of this paper (also an easy read, at least that section): http://research.microsoft.com/en-us/um/people/lamport/pubs/l...
In the conversation with Meijer, Lamport explains that he believes that "linguistic reasoning" 1. requires far more complicated math ("weird, computer science math", like domain theory, category theory, type theory etc.) but, in his opinion, that math doesn't really make reasoning about the algorithm any easier.
All I can say personally is that I find Lamport's view to be a more natural fit with how I think of algorithms (this is entirely subjective), and that learning his formalism to the level where you can specify and reason about very large, very complex real-world systems takes a "plain" engineer maybe two weeks of self study, while learning the more PL-based approaches to reach that level would take a programmer years. This is pretty objective. I can also say that I occasionally see academic papers that describe how to express and reason about some simple properties (like worst-case complexity) in Coq, which would be almost trivial for a TLA+ practitioner, no more than a month after first laying eyes on TLA+. So for me, at least, the difference is a pragmatic one.