5 ms·

Great article, and I look forward to the next! I've been meaning to learn about TLA+ for a while. One thought I didn't see expressed, in all the comparisons of

Great article, and I look forward to the next! I've been meaning to learn about TLA+ for a while. One thought I didn't see expressed, in all the comparisons of tools and approaches, is that sometimes you don't care about time and state. In purely "transformational" programs, like compilers, for example, all state is incidental complexity, so we can analyze them as pure functions. Meanwhile, all the questions such as whether we can just execute the spec and whether we can prove properties of real programs remain. New web frameworks are trying to keep the parts that deal with time and state as small and self-contained as possible, leaving the rest to be described using functions. Couldn't we say that the factor of "do you care about time" is behind observations such as that TLA+ is mostly popular with concurrent and distributed systems, or that approaches that only look at function contracts often apply to pieces of a program but not the whole? As a more specific statement than, for example, that distributed systems are particularly hard so they necessitate particularly powerful tools.

pron 9y ago
> all state is incidental complexity This is an example of the "Whorfian syndrome" of functional programming. Program state is not the same as the problem of "global mutable state" often cited as a cause of programming bugs. When it comes to program analysis, I see no reason why reasoning about state would be any different, let alone more complicated, than reasoning "trasnformationally". It's exactly like the difference between: h(g(f(x))) and let a = f(x) b = g(a) c = h(b) Reasoning about the two is exactly the same, and the program state in both cases is also identical: you have three states. I also disagree that there is no interest in time or space in purely trasformative systems. First, A trasnformative algorithm that is, say, doubly exponential in time or space is just as wrong as a database that fails to give an answer. Second -- and more importantly -- reasoning about a recursive algorithm is exactly like reasoning about state. There is no way to show that Quicksort works without reasoning about state. You may not mention it explicitly in your chosen formalism or you may call it by a different name, but it's there, and you're taking it into consideration. Also, TLA+ is a universal formalism, and, as you'll see in part 2, there's nothing stopping you from representing everything as functions without any passage of time. The reasoning is identical -- there is no added complexity at all, incidental or otherwise -- but may be a matter of personal aesthetic preference. Because TLA+ is a mathematical notation, substitution and "equational reasoning" works just as well even though time can be expressed. I would say that the main difference between TLA+ and the functional approaches, is that in TLA+ you reason purely mathematically, while in the functional approaches you reason within a (complex) programming language. It's very hard to talk about popularity, because, as far as I know, there are no "functional" tools that are used in the industry at all (certainly not without help from academics). Part of the reason may be due to the fact that so far, software companies that require verification usually write reactive realtime software rather than compilers, so they use tools like B-Method, SCADE, SPIN and TLA+. Another reason is that with the exception of the very good, but rather limited Why3, there are simply no industrial-strength verification tools out there aimed at industrial use rather than research.
- dgreensp 9y ago
  I mean "state" in the sense that we can distinguish time-dependent systems with internal state or memory from time-independent systems, whose outputs are a pure function of their inputs. Combining pure functions to create pure functions does not introduce any state, in this sense. An entire program may have no observable state, like a command-line tool that reads stdin and writes stdout with no particular timing. It does have state inside it, of course, but only because it's running on a giant state machine. We can fully describe its behavior without making reference to any internal states, using functions or relations to talk about the relationship between its input and its output. > I would say that the main difference between TLA+ and the functional approaches, is that in TLA+ you reason purely mathematically, while in the functional approaches you reason within a (complex) programming language. This statement puzzles me, because we have great math for reasoning about pure functions (mappings). We have lambda calculus and category theory. You don't need a state machine to prove QuickSort works in a purely mathematical way, either, just statements about the equivalence of functions. The recursion can be handled using the fixed point operator and the algebraic laws it obeys. Edit: In fairness, existing "functional approaches" to specification do seem complex and look like programming languages. I came across an old comment of yours (https://news.ycombinator.com/item?id=11835178 https://news.ycombinator.com/item?id=11835178) that seemed to support the idea that FP and TLA+ have strengths for different kinds of programs, depending on whether they are more transformative or more reactive. I'm just as happy if learning more about TLA+ turns my idea of this on its head, though!
  - pron 9y ago
    > Combining pure functions to create pure functions does not introduce any state, in this sense. Yes, but that's not the same as state in the TLA+ sense. You cannot have computation without state in the TLA+ sense, whether you call your functions pure or not. In TLA+, an algorithm that "purely" computes quicksort and one that outputs an interim result after each recursive step is the same algorithm. TLA+ doesn't talk about visible state, but state in the most fundamental way, without which there is no computation whatsoever. In part 3 I ask whether Euclid's algorithm or Quicksort are imperative or pure-functional. There is no way to answer that question, as their descriptions are at an abstraction level above where this distinction can be made. TLA+ can work at that level. You just can't look at Euclid's algorithm (or quicksort) in TLA+, and tell whether it's imperative or functional. It's an abstract mathematical description. > We have lambda calculus Lambda calculus is a state machine (or, more precisely, it is naturally described as a state machine). > You don't need a state machine to prove QuickSort works in a purely mathematical way, either, just statements about the equivalence of functions. What you're calling state and what TLA+ calls state is not the same thing. Whichever way you prove Quicksort works is the way you'd do it in TLA+ with state. You just don't call it state. I would, however, be very much interested to see how you prove Quicksort works using category theory. AFAIK, all approaches to verify QS work the same way, using an inductive invariant, namely an invariant on state. > that seemed to support the idea that FP and TLA+ have strengths for different kinds of programs I was talking about synchronous programming languages inspired by TLA+, and I agree. I would rather write a compiler in a pure-functional language than in a synchronous one, and an interactive program in a synchronous language than a pure-functional one. But that is a separate discussion from that about mathematical reasoning. I would agree that if one day there would be a FP-based verification tool that is aimed at engineers rather than researchers, then for ergonomics/syntax reasons, it's possible that it would be more convenient for reasoning about compilers. But there's nothing in the theory of TLA+ that makes it less convenient. I do, however, admit that there are tradeoffs between working in "pure math" as in TLA+, or within a programming language. There are often patterns that are specific to certain programming styles, and reasoning within a similar formalism may reduce effort. In other words, sometimes you may want to reason about a specific expression of an algorithm rather than about the algorithm in its pure abstract sense, and a formalism that shares the same expression style may make it easier. But I don't know how much of this is purely hypothetical. Most algorithms that are interesting or subtle, are essentially interesting or subtle, and verifying them in all formalisms is very similar (and usually involves the same proof technique: inductive invariants).

pron 9y ago

> all state is incidental complexity This is an example of the "Whorfian syndrome" of functional programming. Program state is not the same as the problem of "global mutable state" often cited as a cause of programming bugs. When it comes to program analysis, I see no reason why reasoning about state would be any different, let alone more complicated, than reasoning "trasnformationally". It's exactly like the difference between: h(g(f(x))) and let a = f(x) b = g(a) c = h(b) Reasoning about the two is exactly the same, and the program state in both cases is also identical: you have three states. I also disagree that there is no interest in time or space in purely trasformative systems. First, A trasnformative algorithm that is, say, doubly exponential in time or space is just as wrong as a database that fails to give an answer. Second -- and more importantly -- reasoning about a recursive algorithm is exactly like reasoning about state. There is no way to show that Quicksort works without reasoning about state. You may not mention it explicitly in your chosen formalism or you may call it by a different name, but it's there, and you're taking it into consideration. Also, TLA+ is a universal formalism, and, as you'll see in part 2, there's nothing stopping you from representing everything as functions without any passage of time. The reasoning is identical -- there is no added complexity at all, incidental or otherwise -- but may be a matter of personal aesthetic preference. Because TLA+ is a mathematical notation, substitution and "equational reasoning" works just as well even though time can be expressed. I would say that the main difference between TLA+ and the functional approaches, is that in TLA+ you reason purely mathematically, while in the functional approaches you reason within a (complex) programming language. It's very hard to talk about popularity, because, as far as I know, there are no "functional" tools that are used in the industry at all (certainly not without help from academics). Part of the reason may be due to the fact that so far, software companies that require verification usually write reactive realtime software rather than compilers, so they use tools like B-Method, SCADE, SPIN and TLA+. Another reason is that with the exception of the very good, but rather limited Why3, there are simply no industrial-strength verification tools out there aimed at industrial use rather than research.

dgreensp 9y ago
I mean "state" in the sense that we can distinguish time-dependent systems with internal state or memory from time-independent systems, whose outputs are a pure function of their inputs. Combining pure functions to create pure functions does not introduce any state, in this sense. An entire program may have no observable state, like a command-line tool that reads stdin and writes stdout with no particular timing. It does have state inside it, of course, but only because it's running on a giant state machine. We can fully describe its behavior without making reference to any internal states, using functions or relations to talk about the relationship between its input and its output. > I would say that the main difference between TLA+ and the functional approaches, is that in TLA+ you reason purely mathematically, while in the functional approaches you reason within a (complex) programming language. This statement puzzles me, because we have great math for reasoning about pure functions (mappings). We have lambda calculus and category theory. You don't need a state machine to prove QuickSort works in a purely mathematical way, either, just statements about the equivalence of functions. The recursion can be handled using the fixed point operator and the algebraic laws it obeys. Edit: In fairness, existing "functional approaches" to specification do seem complex and look like programming languages. I came across an old comment of yours (https://news.ycombinator.com/item?id=11835178 https://news.ycombinator.com/item?id=11835178) that seemed to support the idea that FP and TLA+ have strengths for different kinds of programs, depending on whether they are more transformative or more reactive. I'm just as happy if learning more about TLA+ turns my idea of this on its head, though!
- pron 9y ago
  > Combining pure functions to create pure functions does not introduce any state, in this sense. Yes, but that's not the same as state in the TLA+ sense. You cannot have computation without state in the TLA+ sense, whether you call your functions pure or not. In TLA+, an algorithm that "purely" computes quicksort and one that outputs an interim result after each recursive step is the same algorithm. TLA+ doesn't talk about visible state, but state in the most fundamental way, without which there is no computation whatsoever. In part 3 I ask whether Euclid's algorithm or Quicksort are imperative or pure-functional. There is no way to answer that question, as their descriptions are at an abstraction level above where this distinction can be made. TLA+ can work at that level. You just can't look at Euclid's algorithm (or quicksort) in TLA+, and tell whether it's imperative or functional. It's an abstract mathematical description. > We have lambda calculus Lambda calculus is a state machine (or, more precisely, it is naturally described as a state machine). > You don't need a state machine to prove QuickSort works in a purely mathematical way, either, just statements about the equivalence of functions. What you're calling state and what TLA+ calls state is not the same thing. Whichever way you prove Quicksort works is the way you'd do it in TLA+ with state. You just don't call it state. I would, however, be very much interested to see how you prove Quicksort works using category theory. AFAIK, all approaches to verify QS work the same way, using an inductive invariant, namely an invariant on state. > that seemed to support the idea that FP and TLA+ have strengths for different kinds of programs I was talking about synchronous programming languages inspired by TLA+, and I agree. I would rather write a compiler in a pure-functional language than in a synchronous one, and an interactive program in a synchronous language than a pure-functional one. But that is a separate discussion from that about mathematical reasoning. I would agree that if one day there would be a FP-based verification tool that is aimed at engineers rather than researchers, then for ergonomics/syntax reasons, it's possible that it would be more convenient for reasoning about compilers. But there's nothing in the theory of TLA+ that makes it less convenient. I do, however, admit that there are tradeoffs between working in "pure math" as in TLA+, or within a programming language. There are often patterns that are specific to certain programming styles, and reasoning within a similar formalism may reduce effort. In other words, sometimes you may want to reason about a specific expression of an algorithm rather than about the algorithm in its pure abstract sense, and a formalism that shares the same expression style may make it easier. But I don't know how much of this is purely hypothetical. Most algorithms that are interesting or subtle, are essentially interesting or subtle, and verifying them in all formalisms is very similar (and usually involves the same proof technique: inductive invariants).