5 ms·

> The programming language theory community indeed tries to make mathematical reasoning explicit, but they're trying to make reasoning possible within the const

by fmap 10y ago

> The programming language theory community indeed tries to make mathematical reasoning explicit, but they're trying to make reasoning possible within the construction language (like the algebra of gears). We discussed this point before, and this comment finally makes it clear to me why we never saw eye to eye. Equational reasoning is a tool for reasoning about programs, but not the only tool. Lamport uses it too, in the form of refinement (this is exactly what is used in practice, outside of "educational" papers about functional programming). More importantly though, nobody insists that all reasoning has to be equational. The Hoare logic and its Owicki-Gries variant for concurrency are the grandfathers of modern program logics, which give you a very precise language (ordinary math + X, same as what Lamport wants) for reasoning about program correctness. The only difference in this paper is that Lamport insists that programs should be syntactically represented as state machines, while most PLT people would insist that this is too much of a restriction. Typed programs enable more abstract programs and specifications, because the abstraction mechanism offered by types is in some sense dual to refinement. Types allow you to restrict client code in a lightweight way. Combined with higher-order functions (i.e., first class functional abstraction), this allows you to achieve more abstract specifications than what can be done with state machines. If I have a program in TLA+, I represent it as a state machine and any specification I write down is essentially just a refinement of this state machine. You cannot really hide internal states, unless you can explicitly skip them via simulation (or at least that is my impression of TLA+, you are far more experienced here and very welcome to contradict me). In a typed programming language, quantification gives you the dual abstraction of restricting the users of your program. Existential types allow you to pick an invariant relation between two implementations. Crucially this invariant does not have to be a (bi)simulation. If you look at this from a state machine perspective, then these can be two completely different state machines externally, but they are different in a way that clients can't exploit. For a concrete example, in https://people.mpi-sws.org/~dreyer/papers/caresl/paper.pdf https://people.mpi-sws.org/~dreyer/papers/caresl/paper.pdf , the authors show refinement between flat combining and locking, as well as between a lockfree and a lock-based stack with iterators. In this generality, this is only sound for typesafe clients. ---- If this sounds overly negative and critical of Lamport's work, then I apologize. The main point I want to make is that we are using substantially the same tools. There is nobody in program verification who seriously insists that equational reasoning is the only tool the world needs. The point of equational reasoning was always that it is a lightweight method which is easily taught to ordinary programmers. That's what makes it valuable. If you encounter a paper (typically by Richard Bird :) ), verifying complicated programs using only equational reasoning, then take this with a grain of salt. The interesting thing about such papers is that it's possible at all ("see how far you can push this idea!"), but I've yet to meet anyone who seriously insists that this is always the easiest proof you can come up with...

pron 10y ago
> The only difference in this paper is that Lamport insists that programs should be syntactically represented as state machines Just to make sure: He does not intend for compilable programs to be represented as TLA formulas, just as electrical circuits are not laid out with ODEs. He says that reasoning about the properties of programs should be done in a system like TLA, just as electrical circuits can be modeled as ODEs. TLA+ itself comes with a tool that lets you write specification in a syntax called PlusCal, which is similar to familiar imperative languages, and Lamport himself says that he made that language because that syntax may be more convenient for some tasks. > while most PLT people would insist that this is too much of a restriction. Reasoning syntactically about a program in its ready-for-construction source has several advantages, but I doubt anyone would view TLA as any sort of a restriction (quite the opposite: it allows to specify discrete dynamical systems that are not even computable). But the main difference for practitioners is this: TLA works today for a wide range of programs. The ideal of reasoning about programs in their source language with similar cost is far from realized. TLA succeeds in practice simply because it is far less ambitious. > Typed programs enable more abstract programs and specifications, because the abstraction mechanism offered by types is in some sense dual to refinement. I am not sure what you mean. > Combined with higher-order functions (i.e., first class functional abstraction), this allows you to achieve more abstract specifications than what can be done with state machines. I am not sure you quite realize how state machines are used in TLA. You can use higher-order functions to your heart's content, as well as higher-order state machines. The machine's are abstract, and what constitutes a state is completely up to you. TLA+ is rich enough that you can write an entire program completely using pure functions, that executes as a single TLA step. But reasoning with functions is a specific level of abstraction. TLA allows you to go arbitrarily higher or lower. Functions are too high an abstraction if you're interested to reason about, say, complexity, and they're too low an abstraction if you want to reason about interaction (where they can only constitute single monadic steps). They may be either too high or too low for concurrency. Of course, you can embed TLA in FP and vice versa, but TLA is "naturally" broader in scope. > You cannot really hide internal states Why not? That's what existential temporal quantification is for. `∃∃ x : F`, means that F performs its observable operation using some internal hidden state, x (∃∃ is usually written as bold ∃) > In a typed programming language, quantification gives you the dual abstraction of restricting the users of your program. I'm not sure exactly what you mean. You can achieve the same thing you can with types in an untyped TLA-based language like TLA+. For example, the typing judgment `f:A->B` is simply a conjunction with the proposition `f ∈ [A → B]` in TLA+. Remember that the environment is also part of the process (or machine). > Crucially this invariant does not have to be a (bi)simulation The concept of bisimulation is a rather complex one designed to explain the difference between trace inclusion and stronger forms of equivalence in algebraic models that do not model state explicitly (like CSP/CCS). In TLA, bisimulation and trace equivalence are the same, and simulation is just trace-inclusion. The famous result "the existence of refinement mapping" by Abadi and Lamport shows that this is complete, namely that any implementation relation "A implements B" can be modeled as "A refines B", which in TLA translates to the familiar implication operator `A ⇒ B`. So there is no such thing as two machines, one implementing the other, that cannot be expressed in this way. > In this generality, this is only sound for typesafe clients Again, in TLA, a "typesafe client" is no more than an assumption about the properties of the client "process". In TLA, a specification often takes the form `◻User ∧ ◻Program` or the equivalent `◻(User ∨ Program)` > That's what makes it valuable. I would say that in practice the opposite holds. TLA+ is used by "ordinary" engineers to reason about systems that are far larger and trickier (concurrent, distributed) than anything that is currently done by engineers using equational reasoning in typed PFP. This advantage may (or may not) be short-lived, but I think the combination of simplicity, ease of learning, and scalability both in size and in scope is precisely TLA's pragmatic edge.

by fmap 10y ago

pron 10y ago

> The only difference in this paper is that Lamport insists that programs should be syntactically represented as state machines Just to make sure: He does not intend for compilable programs to be represented as TLA formulas, just as electrical circuits are not laid out with ODEs. He says that reasoning about the properties of programs should be done in a system like TLA, just as electrical circuits can be modeled as ODEs. TLA+ itself comes with a tool that lets you write specification in a syntax called PlusCal, which is similar to familiar imperative languages, and Lamport himself says that he made that language because that syntax may be more convenient for some tasks. > while most PLT people would insist that this is too much of a restriction. Reasoning syntactically about a program in its ready-for-construction source has several advantages, but I doubt anyone would view TLA as any sort of a restriction (quite the opposite: it allows to specify discrete dynamical systems that are not even computable). But the main difference for practitioners is this: TLA works today for a wide range of programs. The ideal of reasoning about programs in their source language with similar cost is far from realized. TLA succeeds in practice simply because it is far less ambitious. > Typed programs enable more abstract programs and specifications, because the abstraction mechanism offered by types is in some sense dual to refinement. I am not sure what you mean. > Combined with higher-order functions (i.e., first class functional abstraction), this allows you to achieve more abstract specifications than what can be done with state machines. I am not sure you quite realize how state machines are used in TLA. You can use higher-order functions to your heart's content, as well as higher-order state machines. The machine's are abstract, and what constitutes a state is completely up to you. TLA+ is rich enough that you can write an entire program completely using pure functions, that executes as a single TLA step. But reasoning with functions is a specific level of abstraction. TLA allows you to go arbitrarily higher or lower. Functions are too high an abstraction if you're interested to reason about, say, complexity, and they're too low an abstraction if you want to reason about interaction (where they can only constitute single monadic steps). They may be either too high or too low for concurrency. Of course, you can embed TLA in FP and vice versa, but TLA is "naturally" broader in scope. > You cannot really hide internal states Why not? That's what existential temporal quantification is for. `∃∃ x : F`, means that F performs its observable operation using some internal hidden state, x (∃∃ is usually written as bold ∃) > In a typed programming language, quantification gives you the dual abstraction of restricting the users of your program. I'm not sure exactly what you mean. You can achieve the same thing you can with types in an untyped TLA-based language like TLA+. For example, the typing judgment `f:A->B` is simply a conjunction with the proposition `f ∈ [A → B]` in TLA+. Remember that the environment is also part of the process (or machine). > Crucially this invariant does not have to be a (bi)simulation The concept of bisimulation is a rather complex one designed to explain the difference between trace inclusion and stronger forms of equivalence in algebraic models that do not model state explicitly (like CSP/CCS). In TLA, bisimulation and trace equivalence are the same, and simulation is just trace-inclusion. The famous result "the existence of refinement mapping" by Abadi and Lamport shows that this is complete, namely that any implementation relation "A implements B" can be modeled as "A refines B", which in TLA translates to the familiar implication operator `A ⇒ B`. So there is no such thing as two machines, one implementing the other, that cannot be expressed in this way. > In this generality, this is only sound for typesafe clients Again, in TLA, a "typesafe client" is no more than an assumption about the properties of the client "process". In TLA, a specification often takes the form `◻User ∧ ◻Program` or the equivalent `◻(User ∨ Program)` > That's what makes it valuable. I would say that in practice the opposite holds. TLA+ is used by "ordinary" engineers to reason about systems that are far larger and trickier (concurrent, distributed) than anything that is currently done by engineers using equational reasoning in typed PFP. This advantage may (or may not) be short-lived, but I think the combination of simplicity, ease of learning, and scalability both in size and in scope is precisely TLA's pragmatic edge.