4 ms·

>I don't know if I'd use the word disingenuous. Point taken. Programmers may see project uncertainly as less pressing/difficult while formal methods are onerou

>I don't know if I'd use the word disingenuous. Point taken. Programmers may see project uncertainly as less pressing/difficult while formal methods are onerous. How much one or the other depends on details, and how the team frames risk and methods to reduce it. Even on the project side, for example, the Chaos report from the 1990s shows some 40% (60% at small companies) of software projects are cancelled before delivering anything mainly due to scope change and lack of executive support. Both require attention. Both are non-trivial. While we're on formal methods I'd like to solicit your opinion a bit more. I am working on a distributed KV store which I'd like to formally certify. I started with TLA+ except that compared to Dafny, Verdi the gap between spec and implementation is higher. I don't like that. Verdi, in particular, comes with formally verified, shimmable network layers plus the ability to produce runnable code from the Coq spec. My practical assessment is, + Dafny: pros: Refine spec to implementation; provides safety and liveness checks. Can produce runnable code towards testing, Q/A experimentation. - Dafny: cons: The Dafny GIT repo is a mess --- extremely disorganized and therefore hard to simulate examples in papers with the real thing. It's very hard to see what libraries to build on. + Verdi: pros: Like Dafy which came after Verdi, it's focused on refinement: go from spec to more and more implementation detail. It's based on Coq proofs and Coq has tons of books, examples, exercises. See https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/ for five solid write-ups concluding with formally certified C code. So I do not see Verdi as overly academic. It has formally verified libraries that can be re-used esp. in the area of message passing, marshalling which models reliable and non-reliable packet delivery. Moreover, and this is important for distributed programming, proofs can be done in terms of traces. Not sure if TLA+ and it's model checker TLC can do that. - Verdi: Cons: I have to learn Coq, not the end of the world but it's another chunk of work. Also Verdi can't help with liveness checks while TLA+ and Dafny or Spin can. I initially worked with SPIN and TLA+: those specs are checked in a model checker which looks for counter examples. I have a certain feel for that. On the other hand as I understand it out the box, Dafny or Verdi or FRAMA-C use proofs. Now a proof is formal and is help, however, I am unclear if Dafny, or Verdi will give me a counter example if a refinement goes wrong. More specifically, if a refinement is wrong which happens: one is unable to prove a claim - and that's your head's up ... or at some point a run of the executables made will assert a violation of a safety property. I'm not sure. + TLA is of course much used in industry -- so I won't plough that field again. But I wish I knew if it can prove system properties through traces like Verdi because it seems such a natural way to reason about distributed systems. TLA+ of course does liveness and safety checks. All of these are free tools ... including SPIN ... so if one can put the time in you can get a lot of power. That's good to know. Navigating some of the finer details as I suggest here is not so easy when choosing one. For my little project I was thinking Verdi for safety and TLA+ for liveness checks when needed. Please weight in ... I'd love to hear more perspectives.

doonesbury 6y ago
I want to better motivate my question on traces by quoting from a paper I enjoyed reading: https://homes.cs.washington.edu/~ztatlock/pubs/verdi-wilcox-pldi15.pdf https://homes.cs.washington.edu/~ztatlock/pubs/verdi-wilcox-... which gives this example for a distributed lock: mutex(τ ) := τ = τ1 ++ (n1, Grant) ++ τ2 ++ (n2, Grant) ++ τ3 → (n1, Unlock) ∈ τ2 What this safety requirement means is that if the lock is granted in some pending message to host n2 (say delivered or in queue to be delivered) then it must have been proceeded by an unlock message and not on the same host getting the grant --- in fact on the last node who was granted the lock. Here n1, n2 designate hostIds. What I like about this approach, is that Verdi seems to make it quite easy to model and specify in terms of nodes, processes on nodes, and messages between nodes whether on a reliable or non-reliable network. And safety conditions seem to naturally flow, in part, from how messages are ordered when sent. Of course, in an unreliable network which Verdi can model too, they may come out of order requiring more work to de-dup and/or ensure exactly-once-delivery.
pron 6y ago
You might be overthinking this. What you want is a cost-effective way of reaching the correctness you need; i.e. a good bug-found-per-hour rate. Unless you have a lot (years) of experience writing formal proofs, I suggest you try them, first. They generally do not have a good correctness ROI compared to other methods. But nothing and no one can give you an answer without knowing the particulars of your project, the people working on it, and the correctness goals. You'll have to try a few things for a bit and then make up your mind. Just remember that 1. the smaller your project is and the fewer people working on it the less the particular formal method chosen matters, and 2. in formal methods, going from 99.999% correct to 99.9999999% correct can be a 10x factor in cost, so the assumption that more correct = better is generally wrong as there are diminishing returns. Of course, if you just want to do this to learn about formal methods rather than find one that you can frequently use in large projects, then the choice matters even less. In terms of basic principles, the tools you mentioned are much closer to one another than they are different.

doonesbury 6y ago

I want to better motivate my question on traces by quoting from a paper I enjoyed reading: https://homes.cs.washington.edu/~ztatlock/pubs/verdi-wilcox-pldi15.pdf https://homes.cs.washington.edu/~ztatlock/pubs/verdi-wilcox-... which gives this example for a distributed lock: mutex(τ ) := τ = τ1 ++ (n1, Grant) ++ τ2 ++ (n2, Grant) ++ τ3 → (n1, Unlock) ∈ τ2 What this safety requirement means is that if the lock is granted in some pending message to host n2 (say delivered or in queue to be delivered) then it must have been proceeded by an unlock message and not on the same host getting the grant --- in fact on the last node who was granted the lock. Here n1, n2 designate hostIds. What I like about this approach, is that Verdi seems to make it quite easy to model and specify in terms of nodes, processes on nodes, and messages between nodes whether on a reliable or non-reliable network. And safety conditions seem to naturally flow, in part, from how messages are ordered when sent. Of course, in an unreliable network which Verdi can model too, they may come out of order requiring more work to de-dup and/or ensure exactly-once-delivery.

pron 6y ago

You might be overthinking this. What you want is a cost-effective way of reaching the correctness you need; i.e. a good bug-found-per-hour rate. Unless you have a lot (years) of experience writing formal proofs, I suggest you try them, first. They generally do not have a good correctness ROI compared to other methods. But nothing and no one can give you an answer without knowing the particulars of your project, the people working on it, and the correctness goals. You'll have to try a few things for a bit and then make up your mind. Just remember that 1. the smaller your project is and the fewer people working on it the less the particular formal method chosen matters, and 2. in formal methods, going from 99.999% correct to 99.9999999% correct can be a 10x factor in cost, so the assumption that more correct = better is generally wrong as there are diminishing returns. Of course, if you just want to do this to learn about formal methods rather than find one that you can frequently use in large projects, then the choice matters even less. In terms of basic principles, the tools you mentioned are much closer to one another than they are different.