Re: Lamport clocks and special relativity: I don't think Lamport makes it sufficiently clear that the SR analogy is just an analogy and is not physically relevant. It is perfectly valid to treat the computers in a datacenter as a single inertial reference frame, with a natural notion of simultaneity. (Geo-distributed clocks can still be synchronized, since the Schwarzschild solution defines spacelike hypersurfaces with constant time coordinate.) Logical clocks (which totally order events consistent with their causal relations) are useful (because synchronization is hard), but not physically necessary (because synchronization is possible).
Lamport has always been in favor of a rigorous mathematical reasoning about programs, but has always warned against looking for a "new math", the "right kind of math", or a "silver bullet math" (in other talks he calls it "weird computer-science math"), as he believes that ordinary math is all you need. So yeah, Lamport is not a big fan of FP (or any PL theory for that matter). He's been fighting the Robin Milner school of thought, or PL semantics in general since at least the early nineties. He says here that once you deal with all the incidental complexity, you're left with the essential complexity, and that is the hard part, and he's skeptical of the ability of "new math" to help solve the problem.
One major school of thought in formal methods is the type theory tradition. The one-sentence formal methods interpretation of this program is that types are theorems and programs are proofs. The idea, basically, is to choose a type system that is expressive enough to encode interesting properties. Then, if your program has that type, you know that your program is correct with respect to the specification that is encoded in the type. It turns out that there are type theories in which arbitrary mathematical properties can be encoded and proven, so this approach is very versatile. Systems such as Coq, NuPRL, Idris, and Lean are in this tradition.+
Obviously, there are also other approaches to formal methods that are not built upon type theory. However, my experience is that the type theorists have been incredibly productive, so if you spend enough time doing formal methods you'll probably find some work done in the type theory tradition that's useful or relevant to any particular approach.
+
I'm not a type theorist and have reason to believe that certain type theorists would perhaps disagree with this characterization for reason that would be rather difficult for a non-type-theorist to understand, but hopefully this gives you a rough idea.
Also, it's worth noting that those in the Milner tradition see their agenda as being far more than just one approach toward formal methods, and also as not being principally about types. But thinking about that tradition in terms of Coq et al. and props-as-types is the best way to understand its place in Formal Methods.
> However, my experience is that the type theorists have been incredibly productive
They have, but much less so than people in the "temporal logic tradition". Type theory-based formal methods are virtually nonexistent in the industry (and the word virtually could probably be replaced with literally if we don't count joint industry-academia projects), while temporal logic is used to verify thousands of applications every year. The reason you see fewer papers is precisely because the approach is less mature. On the other hand, you find that papers using more traditional approaches are more cited (e.g., Lamport's first TLA paper alone has many more citations than any paper on type theory ever).
It is true, however, that PL theory is about much more than just formal methods (it is first and foremost about programming languages). The problem they're tackling is much harder and more ambitious, but so far they've had little success in the field.
> Type theory-based formal methods are virtually nonexistent in the industry
I mean, all of the ML-derivative languages are in very wide-spread use. I guess you could argue that type systems aren't formal methods, but I'd disagree -- especially in the case of systems with effective type inference, which is essentially a bit of theorem proving baked into your language.
I would guess that Algorithm W (and derivatives) are the most successful and most widely used formal methods tool in the world today.
> ...if we don't count joint industry-academia projects
The same is true for most formal methods (FWIW I consider MSR and similar labs squarely in the "academia" side of that divide...) It's not even clear to me that this is a bad thing, actually. Maybe for highly critical systems it makes sense for companies to contract with boutique formal methods firms.
More generally, what I meant by "incredibly productive" is that a lot of the ideas in their work are equally applicable to other systems that aren't in that tradition. So that even if you aren't working the Milner tradition (which I man not), you may still find this work worth knowing about and borrowing from (which I do).
> I guess you could argue that type systems aren't formal methods, but I'd disagree -- especially in the case of systems with effective type inference, which is essentially a bit of theorem proving baked into your language.
The kind of properties those type systems that are in relatively widespread use prove are not even remotely close to those you'd call "program correctness".
> I would guess that Algorithm W (and derivatives) are the most successful and most widely used formal methods tool in the world today.
OK, but that's an extremely weak formal method; weaker than some static analysis tools, that are also in widespread use.
> The same is true for most formal methods
Not really. SCADE is quite popular in safety-critical hard realtime systems, and TLA+, while far from "popular" is being regularly used at Amazon, Oracle and smaller companies without any assistance from academia. Other tools, like Z and Ada SPARK (both used by Altran), B-Method (popular in railway software) or SPIN are also regularly used in the industry.
> you may still find this work worth knowing about and borrowing from (which I do).
Sure, but it goes both ways. I've seen a paper about proving the correctness of some control systems for quadcopters in Coq, and they basically used Lamport's TLA in Coq.
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.
I've thought of an analogy that demonstrates the difference between the two approaches: Consider an electrical engineer designing an analog circuit and a mechanical engineer designing a contraption made of gears, pulleys and springs. They can use the “standard” mathematical approach, plugging in the equations describing what the components do and get an equation for the system which they can then analyze, or they can invent an algebra of electronic components and an algebra of mechanical components and reason directly in a “language” of capcitors and resistors (one capacitor X plus one resistor Y is equal to capacitor S plus resistor T etc.) and in a language of gears and springs. Lamport’s approach is analogous to the former, while the PL approach is analogous to the latter.
Well, his points about necessary hard math and proving correctness resemble those of many in academia, I can understand your bias. But it is a bias and there isn't even a good argument to support it. Proofs never actually cover absolutely every possible case and we also can have as reliable software without the hard math whatsoever. But going into psychology and thinking about making things easy for humans goes against what is generally accepted in CS research.
>> Proofs never actually cover absolutely every possible case and we also can have as reliable software without the hard math whatsoever.
This is ridiculous. If not being able to prove everything doesn't help, we should get rid of type systems altogether. Programmers are so complacent and ignorant to what their compilers provide them out of the box, they forget how many brilliant people, proofs, and countless hours it took to create those features.
>> But going into psychology and thinking about making things easy for humans goes against what is generally accepted in CS research.
Well, no. Just because you don't understand or care to learn how much pain and work it took to get rid of seemingly arbitrary restrictions of type systems doesn't mean that it is not considered CS research. You think Rust's region types that literally prevent you from leaking memory without garbage collection came out of a hackathon? Java's generics are a usability improvement, isn't it? Do you have any idea about who designed that? Don't even get me started on any of the features in pure languages.
And even if you were so blind to reject all of these as improvements, psychology and usability of programming languages is an actual CS research field with its dedicated conferences. Here's a master's course [0] from University of Cambridge Computer Laboratory.
I don't see a point in your comment, apart from an emotional "people worked hard" stuff. What's your point?
Remember the last couple of bug studies? They didn't show type systems having an effect on reducing number of bugs, but instead showed only significant correlation being number of LOCs. And yet dynamically typed languages require fewer lines to express the same thing.
You see that's what I mean. You have zero understanding of what you're talking about. You think dynamically typed languages came out of thin air? Do you know the difference between a segmentation fault and a dynamic type error?
The point of mathetic's comment was to point out that a lot of ("computer science") mathematics goes into the design of the compilers and interpreters that software engineers use every day. And that it's rather ignorant for a user of one of these modern interpreters or compilers (even of a dynamically typed language!) to claim that this math doesn't matter or isn't useful.
> Remember the last couple of bug studies?
Which studies? There have been at least half a dozen high profile empirical studies about type systems in top tier conferences in the last 5 or 6 years, and probably dozens more in journals/conferences I don't follow.
The empirical evidence is predictably mixed. E.g. Hanenberg has published papers cutting in both directions re: usefulness of type systems.
Also, there's still very little empirical evidence about many type systems. There's a lot of Java vs. X comparison papers, but very few rigorous empirical studies on Haskell or SML or OCaml or Scala, for example. And I'm not aware of a single empirical comparative study on a dependently typed language.
> They didn't show type systems having an effect on reducing number of bugs
Actually, there are empirical studies that show type systems reduce bugs.
Also, as a separate matter, your summation of the available evidence is inaccurate to the point of absurdity. There is not a single shred of empirical evidence for your unconditional claim that type systems don't have an effect on reducing bugs. That hypothesis has never experimentally tested. Furthermore, the empirical data we have suggests that hypothesis is wrong.
Science works by looking at all the evidence and coming to informed conclusions. Cherry picking the N out of M studies that confirm your priors and then generalizing their results far beyond the parameters of the actual study is the opposite of scientific thought.
> but instead showed only significant correlation being number of LOCs.. And yet dynamically typed languages require fewer lines to express the same thing.
My OCaml programs are very often far shorter than my Python programs. Again, your unconditioned claims are getting you in trouble.
You probably mean to say something like "Java programs are usually longer than Python programs", in which case you have a reasonable critique of Java's type system, but not of type systems in general -- or even of the half dozen type systems that are radically different from Java's and in wide-spread use in production environments. And in fact, most adamant supports of type systems are probably some of the most ardent critics of Java's type system, so rejections of type systems on the basis of Java comparisons are a bit of a straw man IMO.
If there's a single thing that ALL of the various empirical PL design researchers could agree on, it's that the sort of unconditioned claims that are made in your post should be avoided.
If there's anyone who works very hard to make formal methods approachable to practitioners, that would be Leslie Lamport. He often says that he's not interested in methods that are not usable by "ordinary" engineers working on large, real-world systems. Amazon now uses his TLA+ to specify and verify many (most?) of their AWS services, and they've learned it all on their own. It's been so successful that managers encourage programmers to use TLA+. This is now spreading to Oracle, too. You can read about Amazon's experience here: http://glat.info/pdf/formal-methods-amazon-2014-11.pdf
I discovered TLA+ when I needed to design a complex distributed database. I learned it in a couple of weeks, and immediately put it to good use. It quickly uncovered some (big!) mistakes in my original idea, and helped me find a solution. So my motivation to learn and use TLA+ was, like Amazon's, 100% pragmatic and not at all academic.
BTW, TLA+ has spread to Oracle because the guy that introduced TLA+ at Amazon (Chris Newcombe) now works at Oracle Cloud (along with a bunch of other senior AWS talent).
Most proofs have assumptions about the system which can be (occasionally/rarely) violated, but which make the proof tractable, or simply don't model features of the real system.
I think the point is that you can have a proof of correctness in a crypto package that doesnt account for power-usage side-channel attacks, for example.
This is true, but beside the point: a library with no proofs about it doesn't solve that problem, and the library with proofs tells me I don't have certain problems for sure.
The question is then: is it worth the proof development effort to only get those partial guarantees? I would argue yes, for a lot of reasons (and high EAL levels tend to agree that it is for high-assurance stuff), but it's a matter of some debate.
I am fairly sure, upon reading this thread, that this is not zzzcpan's point. His point is to denigrate the entire practice if providing proofs. I think he's referring to fields which, given their critical and highly difficult nature, should in fact start with the proofs and work to invalidate the system over increasingly more total domains of implemention.
You're right that you can take a mathematical proof out of the realm of abstract math and it's new domain may not have all the guarantees we need, but this means we need to extend the system to account for the new domain (and within this domain, the proof is not valid).
But the poster doubled down on this idea that "there are constraints proofs ignore" within the existing domain. Outside of convenient proofs that upper division students provide, this is not true.
A good example of this process and the nature of "pure" CS interacting with the real world is the field of distributed databases. As the field has grown, proofs are expected to aggressively model real world conditions and in fact go further, modeling outright adversarial conditions unlikely to occur in the real world.
I was merely reiterating a common (and I think sensible) point that we can't write proofs about things we don't have the computational resources to address or just plain don't realize are an issue. Both are very real challenges to using proofs about our software, and should be kept in mind when talking about the field.
The said, Im a proponent of everything from proofs about abstract algorithm properties to basic model checking on a spec to using formal methods to extract a program with guaranteed propertied from a formal spec we've written proofs about in something like Coq.
DARPA funding HoTT research should clue anyone in that this stuff is useful.
I think we should work to prove software and that's an ongoing process, but it's hard to imagine using an algorithm without a proof of at least correctness and convergence.
I just see people talking about domains and saying, "We don't need proofs for software" like they learned literally nothing from OpenSSL last year. And perhaps they did not, but I think we all should recognize that the stakes are getting pretty high and it's time to stop pretending we're all supervillan-level software designers.
It was an interesting article. Neat how one scheme was inspired by a bakery. The concern with the red light happened to me. Its timing was odd where I wasn't sure if I'd make it or not but on a road with a high speed limit. I decided to brake at the last moment. Should've worked but tires were bald. I landed in the middle of the intersection with a police officer to my right. So, the "hypothetical" example of Lamport cost me money in the real world. ;)
However, I reject his notion that computation is basically digital, step-by-step process. There's actually at least two models of computation where one is continuous. I gave a lot of detail in the link below:
https://channel9.msdn.com/Shows/Going+Deep/E2E-Erik-Meijer-a...