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
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.
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...
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.
nottorp · · focus · HN ↗
Betelbuddy · · focus · HN ↗
Jesus, I cant stand formal methods people...
Jtsummers · · focus · HN ↗
Betelbuddy · · focus · HN ↗
rcxdude · · focus · HN ↗
Betelbuddy · · focus · HN ↗
Apparently their lawyers never got the memo that the tests already guaranteed the software...
rcxdude · · focus · HN ↗
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.