5 ms·

This is a really nice over-view. I'm not from the Milner tradition, but I disagree with your criticisms of that tradition. I think the key difference between

This is a really nice over-view. 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.

pron 10y ago
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.

pron 10y ago

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.