2 ms·

Testers are not selling guarantees...

Jtsummers 9d ago
That's exactly what testers are selling though. If they aren't guaranteeing the program is correct (up to what is tested) then what purpose do they serve? Same with formal methods, offering guarantees up to what is proven.
- Betelbuddy 9d ago
  Oh my my... "Program testing can be used to show the presence of bugs, but never to show their absence" - Edsger Dijkstra
  - Jtsummers 9d ago
    Ah, but you can't stand those formal methods folks, why are you appealing to authority with Edsger Dijkstra?
    - Betelbuddy 9d ago
      You are trying to convince me that because you pressed "A" once on the vending machine and worked, you declare "A" is proven to dispense Coke...
      - Jtsummers 9d ago
        > You are trying to convince me that because you pressed "A" once on the vending machine and worked, you declare "A" is proven to dispense Coke... This thread is hilarious, thank you. You start off saying you "cant [sic] stand formal methods people" and now you're giving an example of why formal methods are useful. And you're appealing to authority using a man who was a major proponent of formal methods. What's your actual position on formal methods?
        Betelbuddy 9d ago
        Have you considered a career is stand up comedy? The quote from Dijkstra stands on its own...quoting a famous person stating something independently demonstrable, does not magically turn the statement into an appeal to authority :-)) >> a man who was a major proponent of formal methods. No he was not, but you see, its irrelevant in the context of the argument you failed to defend. And Dijkstra fails your purity test. He himself wrote that he saw "no specific virtue in being a formalist" and would use formal methods "when I feel they help."
rcxdude 9d ago
Tests are guaranteeing that the product doesn't fail under the test conditions. Formal verification is guaranteeing the product doesn't deviate from the formal spec under a given set of assumptions. Both of them are useful but depend on how well the thing being checked actually correlates with what you care about.
- Betelbuddy 9d ago
  Interesting definition of guarantee....what about the people who run millions of them? Well Microsoft: "AS IS." Apple: "WITH ALL FAULTS" Adobe: "no guarantee of error-free operation." Apparently their lawyers never got the memo that the tests already guaranteed the software...
  - rcxdude 9d ago
    Well yeah, why would they offer an legal guarantee if they don't have to? They could have a watertight proof that their software works perfectly in all situations (lol) but the lawyers still would prefer to disclaim as much liability as possible. And even if they did, all the test guarantee is that the tests pass, of course the main limit is that they don't actually test even a small fraction of what the customers actually want to do.

That's exactly what testers are selling though. If they aren't guaranteeing the program is correct (up to what is tested) then what purpose do they serve? Same with formal methods, offering guarantees up to what is proven.

Betelbuddy 9d ago
Oh my my... "Program testing can be used to show the presence of bugs, but never to show their absence" - Edsger Dijkstra
- Jtsummers 9d ago
  Ah, but you can't stand those formal methods folks, why are you appealing to authority with Edsger Dijkstra?
  - Betelbuddy 9d ago
    You are trying to convince me that because you pressed "A" once on the vending machine and worked, you declare "A" is proven to dispense Coke...
    - Jtsummers 9d ago
      > You are trying to convince me that because you pressed "A" once on the vending machine and worked, you declare "A" is proven to dispense Coke... This thread is hilarious, thank you. You start off saying you "cant [sic] stand formal methods people" and now you're giving an example of why formal methods are useful. And you're appealing to authority using a man who was a major proponent of formal methods. What's your actual position on formal methods?
      - Betelbuddy 9d ago
        Have you considered a career is stand up comedy? The quote from Dijkstra stands on its own...quoting a famous person stating something independently demonstrable, does not magically turn the statement into an appeal to authority :-)) >> a man who was a major proponent of formal methods. No he was not, but you see, its irrelevant in the context of the argument you failed to defend. And Dijkstra fails your purity test. He himself wrote that he saw "no specific virtue in being a formalist" and would use formal methods "when I feel they help."

rcxdude 9d ago

Tests are guaranteeing that the product doesn't fail under the test conditions. Formal verification is guaranteeing the product doesn't deviate from the formal spec under a given set of assumptions. Both of them are useful but depend on how well the thing being checked actually correlates with what you care about.

Betelbuddy 9d ago
Interesting definition of guarantee....what about the people who run millions of them? Well Microsoft: "AS IS." Apple: "WITH ALL FAULTS" Adobe: "no guarantee of error-free operation." Apparently their lawyers never got the memo that the tests already guaranteed the software...
- rcxdude 9d ago
  Well yeah, why would they offer an legal guarantee if they don't have to? They could have a watertight proof that their software works perfectly in all situations (lol) but the lawyers still would prefer to disclaim as much liability as possible. And even if they did, all the test guarantee is that the tests pass, of course the main limit is that they don't actually test even a small fraction of what the customers actually want to do.