4 ms·

> If you're interested in formal proofs, I suggest you read the discussion Should Your Specification Language Be Typed?[1] by Leslie Lamport (Paxos, TLA+) and L

> If you're interested in formal proofs, I suggest you read the discussion Should Your Specification Language Be Typed?[1] by Leslie Lamport (Paxos, TLA+) and Lawrence Paulson (ML, Isabelle). It is very balanced and discusses the relative pros and cons of typed and untyped proofs for formal verification I'm not interested in «balance», because this isn't a political debate, and my formal system choices don't affect anyone but me. What I do care about is convenience: not having to translate between formal systems, ruling out as many unwanted behaviors making as little effort as possible. And the arguments in the paper in favor of the «flexibility» of untyped systems are really arguments for sloppiness. To see why a more constructive approach is better, using an example from the article, instead of saying `i - j >= 0`, I would just say `exists k. i = j + k`. This means that the witness that `i - j >= 0`, namely, their difference `k`, can be used throughout the rest of the proof without recomputing it over and over. > (the closest they come to making a specific recommendation is exploring pluggable optional types). I've never found optional types worth the trouble, precisely because they run into the same issues as CircleCI has experienced with core.typed: they greatly constrain typeless exploratory programming, and bring in few of the benefits of typeful exploratory programming. > I do that in Java. Haskell only brings you marginally closer to the correctness of a sorting algorithm than Java does (if at all) anyway. For something like a sorting algorithm, I'd just carry out the proof by hand. > If I need more formal verification, I use a model checker (JPF in the past, now I'm about to switch to TLA+). (...) I've found that using a model-checker that works directly on the Java code (like JPF) is not an advantage in terms of total effort over one that uses a separate specification language, especially one that's as (relatively) simple as TLA+/+Cal. I'm not going to question your experience. But all of this still seems like a lot effort to me. > That's more myth than reality. HotSpot without any tuning whatsoever performs better than pretty much all managed languages. I never compared HotSpot's performance with any other managed runtime. Mostly because it never gets to the point where a performance comparison matters - I don't care how fast a runtime system is if it's too hard to write correct programs that run on it. > Tuning is required if you need to really come close to C-speeds, and in those cases it still requires far less work than C. But that's a whole other discussion. I never said C. I'm not willing to give up the ability to define my own abstractions in a statically verifiable and enforceable manner. > True, but no one programs Turing machines. Whether term-rewriting is more convenient than mainstream imperative or imperative-functional (i.e. Clojure, ML, Erlang) requires empirical evidence which is so far sorely lacking. Standard ML, with a subset of its reduction relation, is a perfectly usable term rewriting system. One just needs to be aware that, while types as collections of values are sets, types as collections of terms are just presets - not all terms are equal to themselves. > So you'll be happy to learn that you are wrong! TLA+ and friends have been used to verify lots and lots of concurrent and distributed algorithms (as well as hardware cache-coherence protocols) like Paxos, Raft,(fixed) Chord, and many, many others. See [2] and Lamport's Checking a Multithreaded Algorithm with +CAL[3] I've never seen a convincing demonstration of how those algorithms (or anything in the distributed computing literature) can handle concurrent data structures with interesting invariants. All I see when I read those protocols is how to synchronize a single integer or something equally meaningless.

pron 11y ago
> are really arguments for sloppiness The model checker verifies this for you whether you're "sloppy" (most mathematicians wouldn't call it sloppy; just those that work in typed logic systems) or not. > I'd just carry out the proof by hand. Except that the most used sorting algorithm in the world has had a real bug for years. It is very hard to prove by hand (see http://www.envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/ http://www.envisage-project.eu/proving-android-java-and-pyth...). And besides Lamport, Zave and many others have shown that a large number of hand-proofs of complex concurrent algorithms are very often wrong. Even ones with Lemmas and proofs and Guy Steele's and Nir Shavit's names on them (Snark), and even ones that win "best paper" and are adopted by the industry (Chord). Those algorithms had proofs, but the proofs were wrong: http://brooker.co.za/blog/2014/03/08/model-checking.html http://brooker.co.za/blog/2014/03/08/model-checking.html If you could reliable hand-proof complex algorithms, you wouldn't need many of these tools. Lamport has written quite a bit about the difficulty of proofs for modern algorithms. We are talking about specs that can run to 50 pages or so, and proofs that span hundreds of pages. There's no way people can do it by hand, and there's no way Haskell's type system's help is enough to help you prove it by hand. > But all of this still seems like a lot effort to me. It took 30 man years to deductively prove 7500 LOC with a theorem prover! It takes a few days to spec and verify Paxos or fixed Chord. > if it's too hard to write correct programs that run on it. There's a Haskell dialect on the JVM and a good (multithreaded!) OCaml implementation. > All I see when I read those protocols is how to synchronize a single integer or something equally meaningless. That's because those are the examples that fit in a tutorial. Quite a few real specs for real systems in TLA+/Alloy/Spin are available online. Here's one for Alpha's cache-coherence protocol: http://research.microsoft.com/en-us/um/people/lamport/tla/wildfire-challenge.html http://research.microsoft.com/en-us/um/people/lamport/tla/wi... And here are all the verification annotations used to find and fix the TimSort bug: http://www.envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/ http://www.envisage-project.eu/proving-android-java-and-pyth...
- catnaroek 11y ago
  > Except that the most used sorting algorithm in the world has had a real bug for years. It is very hard to prove by hand... If you could reliable hand-proof complex algorithms, you wouldn't need many of these tools. So I just stick to simple data structures and algorithms for the most part. I don't see a real need for something as complex as TimSort, when quicksort and mergesort (or even insertion sort!) are perfectly good algorithms that any high-schooler with a modicum of mathematical talent can understand. It's totally ridiculous to need an automated theorem prover to verify a sorting algorithm. > And besides Lamport, Zave and many others have shown that a large number of hand-proofs of complex concurrent algorithms are very often wrong... Lamport has written quite a bit about the difficulty of proofs for modern algorithms. How often were these proofs formal proofs? By which I mean that the definitions and theorem statements are just pieces of syntax in a formal system, and that the associated proofs are just calculations driven by the formal system's rules? > Even ones with Lemmas and proofs and Guy Steele's and Nir Shavit's names on them (Snark), and even ones that win "best paper" and are adopted by the industry (Chord). I would never assume an algorithm is correct just because it appears on a paper authored by famous people, or because it's widely used in industry. (You wouldn't do drugs just because famous and rich celebrities do, right?) So, unless the proof of correctness of an algorithm is so trivial that I can find the proof on my own given a couple of hints, I will demand fully formal proof. (Yes, this means that the typical CS paper, especially the typical concurrent/distributed computing paper, doesn't convince me of its thesis.) > We are talking about specs that can run to 50 pages or so, and proofs that span hundreds of pages. They're typically that long because they're written in a mix of natural language and mathematical notation, where the former attempts to convey intuition in order to make up for the latter failing to provide rigor. > There's no way people can do it by hand, and there's no way Haskell's type system's help is enough to help you prove it by hand. Agreed. Once we have accepted complexity in our designs, nowhere can salvation be found. So just say no to gratuitous complexity. > There's a Haskell dialect on the JVM Nice. Will check. > and a good (multithreaded!) OCaml implementation. I don't care. OCaml is an ugly language. > Quite a few real specs for real systems in TLA+/Alloy/Spin are available online. Here's one for Alpha's cache-coherence protocol Any examples that a non-hardware person can appreciate? (Preferably databases, but operating systems would also be okay.)

pron 11y ago

> are really arguments for sloppiness The model checker verifies this for you whether you're "sloppy" (most mathematicians wouldn't call it sloppy; just those that work in typed logic systems) or not. > I'd just carry out the proof by hand. Except that the most used sorting algorithm in the world has had a real bug for years. It is very hard to prove by hand (see http://www.envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/ http://www.envisage-project.eu/proving-android-java-and-pyth...). And besides Lamport, Zave and many others have shown that a large number of hand-proofs of complex concurrent algorithms are very often wrong. Even ones with Lemmas and proofs and Guy Steele's and Nir Shavit's names on them (Snark), and even ones that win "best paper" and are adopted by the industry (Chord). Those algorithms had proofs, but the proofs were wrong: http://brooker.co.za/blog/2014/03/08/model-checking.html http://brooker.co.za/blog/2014/03/08/model-checking.html If you could reliable hand-proof complex algorithms, you wouldn't need many of these tools. Lamport has written quite a bit about the difficulty of proofs for modern algorithms. We are talking about specs that can run to 50 pages or so, and proofs that span hundreds of pages. There's no way people can do it by hand, and there's no way Haskell's type system's help is enough to help you prove it by hand. > But all of this still seems like a lot effort to me. It took 30 man years to deductively prove 7500 LOC with a theorem prover! It takes a few days to spec and verify Paxos or fixed Chord. > if it's too hard to write correct programs that run on it. There's a Haskell dialect on the JVM and a good (multithreaded!) OCaml implementation. > All I see when I read those protocols is how to synchronize a single integer or something equally meaningless. That's because those are the examples that fit in a tutorial. Quite a few real specs for real systems in TLA+/Alloy/Spin are available online. Here's one for Alpha's cache-coherence protocol: http://research.microsoft.com/en-us/um/people/lamport/tla/wildfire-challenge.html http://research.microsoft.com/en-us/um/people/lamport/tla/wi... And here are all the verification annotations used to find and fix the TimSort bug: http://www.envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/ http://www.envisage-project.eu/proving-android-java-and-pyth...

catnaroek 11y ago
> Except that the most used sorting algorithm in the world has had a real bug for years. It is very hard to prove by hand... If you could reliable hand-proof complex algorithms, you wouldn't need many of these tools. So I just stick to simple data structures and algorithms for the most part. I don't see a real need for something as complex as TimSort, when quicksort and mergesort (or even insertion sort!) are perfectly good algorithms that any high-schooler with a modicum of mathematical talent can understand. It's totally ridiculous to need an automated theorem prover to verify a sorting algorithm. > And besides Lamport, Zave and many others have shown that a large number of hand-proofs of complex concurrent algorithms are very often wrong... Lamport has written quite a bit about the difficulty of proofs for modern algorithms. How often were these proofs formal proofs? By which I mean that the definitions and theorem statements are just pieces of syntax in a formal system, and that the associated proofs are just calculations driven by the formal system's rules? > Even ones with Lemmas and proofs and Guy Steele's and Nir Shavit's names on them (Snark), and even ones that win "best paper" and are adopted by the industry (Chord). I would never assume an algorithm is correct just because it appears on a paper authored by famous people, or because it's widely used in industry. (You wouldn't do drugs just because famous and rich celebrities do, right?) So, unless the proof of correctness of an algorithm is so trivial that I can find the proof on my own given a couple of hints, I will demand fully formal proof. (Yes, this means that the typical CS paper, especially the typical concurrent/distributed computing paper, doesn't convince me of its thesis.) > We are talking about specs that can run to 50 pages or so, and proofs that span hundreds of pages. They're typically that long because they're written in a mix of natural language and mathematical notation, where the former attempts to convey intuition in order to make up for the latter failing to provide rigor. > There's no way people can do it by hand, and there's no way Haskell's type system's help is enough to help you prove it by hand. Agreed. Once we have accepted complexity in our designs, nowhere can salvation be found. So just say no to gratuitous complexity. > There's a Haskell dialect on the JVM Nice. Will check. > and a good (multithreaded!) OCaml implementation. I don't care. OCaml is an ugly language. > Quite a few real specs for real systems in TLA+/Alloy/Spin are available online. Here's one for Alpha's cache-coherence protocol Any examples that a non-hardware person can appreciate? (Preferably databases, but operating systems would also be okay.)