4 ms·

If you don't use formal methods, how do you know when your work is done?

by thanksforfish 6y ago

im3w1l 6y ago
When the checks clear.
- ternaryoperator 6y ago
  One of the finest puns I've seen on HN ever!
bluGill 6y ago
When the rate of bugs coming in from test goes below some threshold that your boss is comfortable with. Note that formal methods don't get around this as they do nothing for the class of bugs where it works as specified but now that we see it in operation we know the specification was wrong. (once the spec is right though it is faster)
deleted 6y ago
[deleted]
oldgradstudent 6y ago
If you do use formal methods, how do you know you completed the proof?
- MaxBarraclough 6y ago
  I don't follow. The proof is complete when all proof obligations have been discharged.
  - oldgradstudent 6y ago
    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 6y 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 6y 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 6y 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...
- lmm 6y ago
  You have an automatic tool that tells you. Your program won't "compile" unless the proof is correct. Whether you've proven the right thing still requires judgement - what you end up with is a provably correct implementation of what you thought you wanted. But that's a much smaller problem, and at a minimum you're guaranteed to have an unambiguous definition of what it is you actually built.
  - oldgradstudent 6y ago
    > Whether you've proven the right thing still requires judgement That's my point. Formal methods don't make bugs or debugging disappear. They move it to different domain - the development of the proof. > what you end up with is a provably correct implementation of what you thought you wanted. You end up with a provably correct implementation of what you thought you stated on what you thought you wanted. Serious proofs are highly non-trivial. I've seen experts debate the exact semantics of the most simple properties.
    - lmm 6y ago
      > Formal methods don't make bugs or debugging disappear. They move it to different domain - the development of the proof. They make the thing we usually call bugs and usually experience as debugging disappear. The thing that remains is a very different activity with very different properties.
      - oldgradstudent 6y ago
        > The thing that remains is a very different activity with very different properties. Do you write a correct formal spec the first time round? I don't. Proofs sometimes pass or fail when they shouldn't. When these problem occur I call them bugs, and I call process of finding and fixing them debugging.
        lmm 6y ago
        > When these problem occur I call them bugs, and I call process of finding and fixing them debugging. What do you find it has in common with the activities that we normally call debugging? For me debugging is characteristically about understanding how a system is behaving, essentially by bisecting: it's all about figuring out what should be the case at each point and identifying the point at which things start to go wrong. Whereas correcting a proof is very different: you immediately know where the problem is, and it's more about coming up with a new lemma or strategy - it's the same kind of activity as writing a new proof/program, whereas (traditional) debugging is very much a separate skill, IME.

If you don't use formal methods, how do you know when your work is done?

im3w1l 6y ago

When the checks clear.

ternaryoperator 6y ago
One of the finest puns I've seen on HN ever!

bluGill 6y ago

When the rate of bugs coming in from test goes below some threshold that your boss is comfortable with. Note that formal methods don't get around this as they do nothing for the class of bugs where it works as specified but now that we see it in operation we know the specification was wrong. (once the spec is right though it is faster)

deleted 6y ago

[deleted]

oldgradstudent 6y ago

If you do use formal methods, how do you know you completed the proof?

MaxBarraclough 6y ago
I don't follow. The proof is complete when all proof obligations have been discharged.
- oldgradstudent 6y ago
  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 6y 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 6y 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 6y 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...
lmm 6y ago
You have an automatic tool that tells you. Your program won't "compile" unless the proof is correct. Whether you've proven the right thing still requires judgement - what you end up with is a provably correct implementation of what you thought you wanted. But that's a much smaller problem, and at a minimum you're guaranteed to have an unambiguous definition of what it is you actually built.
- oldgradstudent 6y ago
  > Whether you've proven the right thing still requires judgement That's my point. Formal methods don't make bugs or debugging disappear. They move it to different domain - the development of the proof. > what you end up with is a provably correct implementation of what you thought you wanted. You end up with a provably correct implementation of what you thought you stated on what you thought you wanted. Serious proofs are highly non-trivial. I've seen experts debate the exact semantics of the most simple properties.
  - lmm 6y ago
    > Formal methods don't make bugs or debugging disappear. They move it to different domain - the development of the proof. They make the thing we usually call bugs and usually experience as debugging disappear. The thing that remains is a very different activity with very different properties.
    - oldgradstudent 6y ago
      > The thing that remains is a very different activity with very different properties. Do you write a correct formal spec the first time round? I don't. Proofs sometimes pass or fail when they shouldn't. When these problem occur I call them bugs, and I call process of finding and fixing them debugging.
      - lmm 6y ago
        > When these problem occur I call them bugs, and I call process of finding and fixing them debugging. What do you find it has in common with the activities that we normally call debugging? For me debugging is characteristically about understanding how a system is behaving, essentially by bisecting: it's all about figuring out what should be the case at each point and identifying the point at which things start to go wrong. Whereas correcting a proof is very different: you immediately know where the problem is, and it's more about coming up with a new lemma or strategy - it's the same kind of activity as writing a new proof/program, whereas (traditional) debugging is very much a separate skill, IME.