4 ms·

But how do you know you have the right proof obligations? It's very easy to discharge a massive number of proof obligations while proving nothing of interest.

But how do you know you have the right proof obligations? It's very easy to discharge a massive number of proof obligations while proving nothing of interest. Formal methods don't just make bugs and debugging disappear, they just move it to a different domain - the development of the proofs.

MaxBarraclough 7y ago
I can't make sense of what you're saying. You've completed the proofs when you've discharged all proof obligations. The proof obligations will depend on the formal modelling system you use (Event-B, say), and of course on your formal model. You aren't left in a state of uncertainty as to whether you've finished discharging the proof obligations. Are you referring to the possibility of errors in your model? That's not the same thing.
- oldgradstudent 7y ago
  > Are you referring to the possibility of errors in your model? That's not the same thing. It is very easy to complete a proof on the wrong model, and there are always errors in the model, at least initially. There's always an iterative process of refining the model until you are confident in its being good enough. When are you confident it is good enough? That's quite similar to asking "If you don't use formal methods, how do you know when your work is done?"
  - MaxBarraclough 7y ago
    > It is very easy to complete a proof on the wrong model That doesn't sound right. Automatic proof assistants/verifiers won't approve your proof unless it really is a proof for the model, right? > there are always errors in the model, at least initially Agreed. > There's always an iterative process of refining the model until you are confident in its being good enough. When are you confident it is good enough? It's true that bugs in the model are a possibility. More broadly, it's possible for defects to get through a formal software-development methodology. There was an interesting case study done on this. [0] Vastly fewer than if formal methods are not used, but you're still right that ultimately it's not a completely rock-solid guarantee. (And that's not counting things like bugs in the proof-assistant, or bugs in the non-verified compiler you end up using.) [0] https://www.adacore.com/tokeneer https://www.adacore.com/tokeneer ('Analysis' section is on page 59 of PDF) See also https://blog.adacore.com/tokeneer-fully-verified-with-spark-2014 https://blog.adacore.com/tokeneer-fully-verified-with-spark-... , https://github.com/AdaCore/spark2014/tree/master/testsuite/gnatprove/tests/tokeneer https://github.com/AdaCore/spark2014/tree/master/testsuite/g...

MaxBarraclough 7y ago

I can't make sense of what you're saying. You've completed the proofs when you've discharged all proof obligations. The proof obligations will depend on the formal modelling system you use (Event-B, say), and of course on your formal model. You aren't left in a state of uncertainty as to whether you've finished discharging the proof obligations. Are you referring to the possibility of errors in your model? That's not the same thing.

oldgradstudent 7y ago
> Are you referring to the possibility of errors in your model? That's not the same thing. It is very easy to complete a proof on the wrong model, and there are always errors in the model, at least initially. There's always an iterative process of refining the model until you are confident in its being good enough. When are you confident it is good enough? That's quite similar to asking "If you don't use formal methods, how do you know when your work is done?"
- MaxBarraclough 7y ago
  > It is very easy to complete a proof on the wrong model That doesn't sound right. Automatic proof assistants/verifiers won't approve your proof unless it really is a proof for the model, right? > there are always errors in the model, at least initially Agreed. > There's always an iterative process of refining the model until you are confident in its being good enough. When are you confident it is good enough? It's true that bugs in the model are a possibility. More broadly, it's possible for defects to get through a formal software-development methodology. There was an interesting case study done on this. [0] Vastly fewer than if formal methods are not used, but you're still right that ultimately it's not a completely rock-solid guarantee. (And that's not counting things like bugs in the proof-assistant, or bugs in the non-verified compiler you end up using.) [0] https://www.adacore.com/tokeneer https://www.adacore.com/tokeneer ('Analysis' section is on page 59 of PDF) See also https://blog.adacore.com/tokeneer-fully-verified-with-spark-2014 https://blog.adacore.com/tokeneer-fully-verified-with-spark-... , https://github.com/AdaCore/spark2014/tree/master/testsuite/gnatprove/tests/tokeneer https://github.com/AdaCore/spark2014/tree/master/testsuite/g...