5 ms·

I would say that the premise of this article is a bit wrong. Naturally the examples given about the language usage in physics do look odd because these are very

I would say that the premise of this article is a bit wrong. Naturally the examples given about the language usage in physics do look odd because these are very simple examples based on the form of the writing that has been agreed on long time ago. Now when we evaluate something more elaborate then we will suddenly discover that there are multiple ways to write down some very fundamental concepts. For example Maxwell equations can be written in many different forms http://www.maxwells-equations.com/forms.php http://www.maxwells-equations.com/forms.php So in fact the language is a very important tool even in physics. Even the author continues and defines a new language to express the relations between and in the state machines. Nonetheless this is an interesting piece of the writing.

pron 10y ago
It's a bit of a subtle point, but it is hard precisely because physics doesn't quite have anything that is analogous to programming languages, and Lamport does draw a distinction between a universal formalism -- "ordinary" math -- and a programming language, which is something that is far more complex. The different forms of Maxwell's equations you present are all very much written in the same language of multivariate calculus (but in different words). I would present Lamport's thesis like this: engineering disciplines usually use a different formalism to reason about system from the one they use to construct it. Consider an electrical engineer designing an analog circuit, and a mechanical engineer designing a contraption made of gears, pulleys and springs. When reasoning about their designs, they can either use the “standard” mathematical approach, plugging in the equations describing what the components do, or invent an algebra of electronic components and an algebra of mechanical components and reason directly in a “language” of capcitors and resistors (one capacitor plus one resistor etc.) or a language of gears and springs. The engineers obviously use a domain-specific tool to design the low-level details of the system, but they use standard math to reason about it (to guide their high-level design and to make sure it achieves what they want). Lamport suggests that software engineers do the same. In practice, most software engineers reason about designs only informally, and even then mostly in their heads. This is fine for simple things, but very hard to do when more complex software systems are concerned. The software verification (academic community) indeed uses an approach similar to Lamport (which uses more-or-less simple math to reason about programs), but they hide the techniques from the user, exposing them merely to the results in a sort of a CAD tool. 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). There are a few advantages to that approach, but one major disadvantage: because programming languages, as Lamport notes, are so complex, the mathematics required to reason about them syntactically is very arcane and extremely complex; it is very much a completely new math. And because it is so new and so complex, PLT researchers have not yet been able to accomplish the task. Reasoning in that new math is currently much harder and much more limited that in Lamport's "simple math" approach[1]. Of course, it's possible that PLT will come up with good solutions in the future. But in addition to the big pragmatic advantage of Lamport's approach (which may be temporary), he claims that using the universal language of "ordinary" math helps find the great similarities between different programs that can be written in many different ways, but are essentially the same. This helps to better understand what computation is, and also helps focus on the core issue -- how the program's environment behaves, how the program interacts with it, and why the program's behavior achieves its goals -- rather than being distracted right from the beginning by details such as the choice of abstractions (which are important only after the core issues are understood). [1]: I sometimes see academic papers about how to reason about pretty basic program properties in Coq that would never be written about Lamport's TLA+ for the simple reason that an ordinary engineer would find them almost trivial in TLA+ after only a month or so since first encountering it.
- 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

It's a bit of a subtle point, but it is hard precisely because physics doesn't quite have anything that is analogous to programming languages, and Lamport does draw a distinction between a universal formalism -- "ordinary" math -- and a programming language, which is something that is far more complex. The different forms of Maxwell's equations you present are all very much written in the same language of multivariate calculus (but in different words). I would present Lamport's thesis like this: engineering disciplines usually use a different formalism to reason about system from the one they use to construct it. Consider an electrical engineer designing an analog circuit, and a mechanical engineer designing a contraption made of gears, pulleys and springs. When reasoning about their designs, they can either use the “standard” mathematical approach, plugging in the equations describing what the components do, or invent an algebra of electronic components and an algebra of mechanical components and reason directly in a “language” of capcitors and resistors (one capacitor plus one resistor etc.) or a language of gears and springs. The engineers obviously use a domain-specific tool to design the low-level details of the system, but they use standard math to reason about it (to guide their high-level design and to make sure it achieves what they want). Lamport suggests that software engineers do the same. In practice, most software engineers reason about designs only informally, and even then mostly in their heads. This is fine for simple things, but very hard to do when more complex software systems are concerned. The software verification (academic community) indeed uses an approach similar to Lamport (which uses more-or-less simple math to reason about programs), but they hide the techniques from the user, exposing them merely to the results in a sort of a CAD tool. 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). There are a few advantages to that approach, but one major disadvantage: because programming languages, as Lamport notes, are so complex, the mathematics required to reason about them syntactically is very arcane and extremely complex; it is very much a completely new math. And because it is so new and so complex, PLT researchers have not yet been able to accomplish the task. Reasoning in that new math is currently much harder and much more limited that in Lamport's "simple math" approach[1]. Of course, it's possible that PLT will come up with good solutions in the future. But in addition to the big pragmatic advantage of Lamport's approach (which may be temporary), he claims that using the universal language of "ordinary" math helps find the great similarities between different programs that can be written in many different ways, but are essentially the same. This helps to better understand what computation is, and also helps focus on the core issue -- how the program's environment behaves, how the program interacts with it, and why the program's behavior achieves its goals -- rather than being distracted right from the beginning by details such as the choice of abstractions (which are important only after the core issues are understood). [1]: I sometimes see academic papers about how to reason about pretty basic program properties in Coq that would never be written about Lamport's TLA+ for the simple reason that an ordinary engineer would find them almost trivial in TLA+ after only a month or so since first encountering it.

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...