5 ms·

I really like his point(s) about mathematics and programming, as he talks about functional programming, especially at 47:20.

by js8 10y ago

pron 10y ago
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. See: http://research.microsoft.com/en-us/um/people/lamport/pubs/state-machine.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/s...
- nickpsecurity 10y ago
  "He's been fighting the Robin Milner school of thought, or PL semantics in general since at least the early nineties. " What does that mean for those of us that follow the formal methods at a high-level?
  - throwaway729 10y ago
    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.
    - pron 10y ago
      > 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.
      - throwaway729 10y ago
        > 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).
        pron 10y ago
        > 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.
  - pron 10y ago
    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). 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/lamport-composition.pdf 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.
    - Confusion 10y ago
      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
  - pron 10y ago
    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.
- deleted 10y ago
  [deleted]
zzzcpan 10y ago
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.
- KirinDave 10y ago
  > Proofs never actually cover absolutely every possible case That's precisely what you need to do in order to have a valid proof. I'm not sure why you'd say this?
  - SomeStupidPoint 10y ago
    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.
    - KirinDave 10y ago
      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 really like his point(s) about mathematics and programming, as he talks about functional programming, especially at 47:20.

by js8 10y ago

I really like his point(s) about mathematics and programming, as he talks about functional programming, especially at 47:20.

pron 10y ago

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. See: http://research.microsoft.com/en-us/um/people/lamport/pubs/state-machine.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/s...

nickpsecurity 10y ago
"He's been fighting the Robin Milner school of thought, or PL semantics in general since at least the early nineties. " What does that mean for those of us that follow the formal methods at a high-level?
- throwaway729 10y ago
  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.
  - pron 10y ago
    > 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.
    - throwaway729 10y ago
      > 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).
      - pron 10y ago
        > 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.
- pron 10y ago
  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). 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/lamport-composition.pdf 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.
  - Confusion 10y ago
    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
- pron 10y ago
  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.
deleted 10y ago
[deleted]

zzzcpan 10y ago

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.

KirinDave 10y ago
> Proofs never actually cover absolutely every possible case That's precisely what you need to do in order to have a valid proof. I'm not sure why you'd say this?
- SomeStupidPoint 10y ago
  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.
  - KirinDave 10y ago
    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.