4 ms·

I never really got how proofs are supposed to solve this issue. I think that would just move the bugs from the code into the proof definition. Your code may d

by cochne 3y ago

I never really got how proofs are supposed to solve this issue. I think that would just move the bugs from the code into the proof definition. Your code may do what the proof says, but how do you know what the proof says is what you actually want to happen?

dgacmu 3y ago
Not really. Imagine the proof says: "in this protocol, when there are more than 0 participants, exactly one participant holds the lock at any time" It might be wrong, but it's pretty easy to inspect and has a much higher chance of being right than your code does. You then use proof refinement to eventually link this very high level statement down to the code implementing it. That's the vision, at least, and it's sometimes possible to achieve it. See, for example, Ironfleet: https://www.microsoft.com/en-us/research/publication/ironfleet-proving-practical-distributed-systems-correct/ https://www.microsoft.com/en-us/research/publication/ironfle...
MaxBarraclough 3y ago
A formal spec isn't just ordinary source-code by another name, it's at a quite different level of abstraction, and (hopefully) it will be proven that its invariants always hold. (This is a separate step from proving that the model corresponds to the ultimate deliverable of the formal development process, be that source-code or binary.) Bugs in the formal spec aren't impossible, but use of formal methods doesn't prevent you from doing acceptance testing as well. In practice, there's a whole methodology at work, not just blind trust in the formal spec. Software developed using formal methods is generally assured to be free of runtime errors at the level of the target language (divide-by-zero, dereferencing NULL, out-of-bounds array access, etc). This is a pretty significant advantage, and applies even if there's a bug in the spec. Disclaimer: I'm very much not an expert. Interesting reading: * An interesting case-study, albeit from a non-impartial source [PDF] https://www.adacore.com/uploads/downloads/Tokeneer_Report.pdf https://www.adacore.com/uploads/downloads/Tokeneer_Report.pd... * An introduction to the Event-B formal modelling method [PDF] https://www.southampton.ac.uk/~tsh2n14/publications/chapters/eventb-dbook13.pdf https://www.southampton.ac.uk/~tsh2n14/publications/chapters...
- xmprt 3y ago
  I think the reason that formal proofs haven't really caught on is because it's just adding more complexity and stuff to maintain. The list of things that need to be maintained just keeps growing: code, tests, deployment tooling, configs, environments, etc. And now add a formal proof onto that. If the user changes their requirements then the proof needs to change. A lot of code changes will probably necessitate a proof change as well. And it doesn't even eliminate bugs because the formal proof could include a bug too. I suppose it could help in trivial cases like sanity checking that a value isn't null or that a lock is only held by a single thread but it seems like a lot of those checks are already integrated in build tooling in one way or another.
  - MaxBarraclough 3y ago
    > more complexity and stuff to maintain Yes, with the current state of the art, adopting formal methods means adopting a radically different approach to software development. For 'rapid application development' work, it isn't going to be a good choice. It's only a real consideration if you're serious about developing ultra-low-defect software (to use a term from the AdaCore folks). > it doesn't even eliminate bugs because the formal proof could include a bug too This is rather dismissive. Formal methods have been successfully used in various life-critical software systems, such as medical equipment and avionics. As I said above, formal methods can eliminate all 'runtime errors' (like out-of-bounds array access), and there's a lot of power in formally guaranteeing that the model's invariants are never broken. > I suppose it could help in trivial cases like sanity checking that a value isn't null or that a lock is only held by a single thread No, this doesn't accurately reflect how formal methods work. I suggest taking a look at the PDFs I linked above. For one thing, formal modelling is not done using a programming language.
  - valand 3y ago
    You mix up development problem with computational problem. If you can't use formal proof just because the user can't be arsed to wait where it is supposed to be necessary, then the software project conception is simply not well designed.
- 3y ago

by cochne 3y ago

dgacmu 3y ago

Not really. Imagine the proof says: "in this protocol, when there are more than 0 participants, exactly one participant holds the lock at any time" It might be wrong, but it's pretty easy to inspect and has a much higher chance of being right than your code does. You then use proof refinement to eventually link this very high level statement down to the code implementing it. That's the vision, at least, and it's sometimes possible to achieve it. See, for example, Ironfleet: https://www.microsoft.com/en-us/research/publication/ironfleet-proving-practical-distributed-systems-correct/ https://www.microsoft.com/en-us/research/publication/ironfle...

MaxBarraclough 3y ago

A formal spec isn't just ordinary source-code by another name, it's at a quite different level of abstraction, and (hopefully) it will be proven that its invariants always hold. (This is a separate step from proving that the model corresponds to the ultimate deliverable of the formal development process, be that source-code or binary.) Bugs in the formal spec aren't impossible, but use of formal methods doesn't prevent you from doing acceptance testing as well. In practice, there's a whole methodology at work, not just blind trust in the formal spec. Software developed using formal methods is generally assured to be free of runtime errors at the level of the target language (divide-by-zero, dereferencing NULL, out-of-bounds array access, etc). This is a pretty significant advantage, and applies even if there's a bug in the spec. Disclaimer: I'm very much not an expert. Interesting reading: * An interesting case-study, albeit from a non-impartial source [PDF] https://www.adacore.com/uploads/downloads/Tokeneer_Report.pdf https://www.adacore.com/uploads/downloads/Tokeneer_Report.pd... * An introduction to the Event-B formal modelling method [PDF] https://www.southampton.ac.uk/~tsh2n14/publications/chapters/eventb-dbook13.pdf https://www.southampton.ac.uk/~tsh2n14/publications/chapters...

xmprt 3y ago
I think the reason that formal proofs haven't really caught on is because it's just adding more complexity and stuff to maintain. The list of things that need to be maintained just keeps growing: code, tests, deployment tooling, configs, environments, etc. And now add a formal proof onto that. If the user changes their requirements then the proof needs to change. A lot of code changes will probably necessitate a proof change as well. And it doesn't even eliminate bugs because the formal proof could include a bug too. I suppose it could help in trivial cases like sanity checking that a value isn't null or that a lock is only held by a single thread but it seems like a lot of those checks are already integrated in build tooling in one way or another.
- MaxBarraclough 3y ago
  > more complexity and stuff to maintain Yes, with the current state of the art, adopting formal methods means adopting a radically different approach to software development. For 'rapid application development' work, it isn't going to be a good choice. It's only a real consideration if you're serious about developing ultra-low-defect software (to use a term from the AdaCore folks). > it doesn't even eliminate bugs because the formal proof could include a bug too This is rather dismissive. Formal methods have been successfully used in various life-critical software systems, such as medical equipment and avionics. As I said above, formal methods can eliminate all 'runtime errors' (like out-of-bounds array access), and there's a lot of power in formally guaranteeing that the model's invariants are never broken. > I suppose it could help in trivial cases like sanity checking that a value isn't null or that a lock is only held by a single thread No, this doesn't accurately reflect how formal methods work. I suggest taking a look at the PDFs I linked above. For one thing, formal modelling is not done using a programming language.
- valand 3y ago
  You mix up development problem with computational problem. If you can't use formal proof just because the user can't be arsed to wait where it is supposed to be necessary, then the software project conception is simply not well designed.
3y ago