It will prove the bugs were corrected implemented... :-) And that your mistaken specification of the tax rules in Switzerland, was correctly translated to code, and that your mistaken specification of the process to request a mortgage is mathematically valid...and that your wrong logic about how much centrifugal force your rocket will be able to stand on ascent was mathematically translated to proven correct code running the incorrect logic...
I presume you also can't stand people who write software tests for similar reasons? The test is wrong, the code is wrong. The spec is wrong, the code is wrong. What a waste of effort! Just write correct code people! Verification is left as an exercise for the end users. Who cares about them anyways? /s
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.
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...
> 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?
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."
nottorp · · focus · HN ↗
Betelbuddy · · focus · HN ↗
Jesus, I cant stand formal methods people...
Jtsummers · · focus · HN ↗
Betelbuddy · · focus · HN ↗
Jtsummers · · focus · HN ↗
Betelbuddy · · focus · HN ↗
"Program testing can be used to show the presence of bugs, but never to show their absence"
Jtsummers · · focus · HN ↗
Betelbuddy · · focus · HN ↗
Jtsummers · · focus · HN ↗
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 · · focus · HN ↗
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."