4 ms·

Surely code you haven't proved correct is going to have way more bugs in it than code you tried to prove is correct? Maybe I'm misunderstanding but this quote i

Surely code you haven't proved correct is going to have way more bugs in it than code you tried to prove is correct? Maybe I'm misunderstanding but this quote is always posted as if it's some kind of rebuttal against formal methods.

jon-wood 11y ago
I think the point he was making is that while its been proven to correctly do what it was built to do, that may not actually be anything like what the user needs it to do. How many intricately specified software projects have failed because the spec bore no correlation to user needs?
DawkinsGawd 11y ago
I always thought that correctness (in computer science) only asserted that an algorithm acted as specified. For example, say the specification was: The input accepts an element in the set of real numbers, and the corresponding output is that number added to the next element in the set of natural numbers. If this algorithm is used to dispense some type of medication, and I enter 3.1 and it murders you with 10 grams of alprazolam... well.... the algorithm is still correct.
- seanwilson 11y ago
  > I always thought that correctness (in computer science) only asserted that an algorithm acted as specified. For example, say the specification was: The input accepts an element in the set of real numbers, and the corresponding output is that number added to the next element in the set of natural numbers. Nobody is saying the formal proof approach will find all bugs, just that it helps find more bugs compared to not using it. You could make the same argument with acceptance testing: unless you specifically tried 3.1 as the input during testing, it might not give you the output you expect. Formal proof can be complimentary to traditional automated tests and QA.
taneq 11y ago
I've always parsed this quote as "Beware of bugs in the above code; I have only proved that the code is correct, I haven't actually compiled and tested it." For any non-trivial code, no matter how much formal analysis you do, you don't trust it until it's been properly tested.

jon-wood 11y ago

I think the point he was making is that while its been proven to correctly do what it was built to do, that may not actually be anything like what the user needs it to do. How many intricately specified software projects have failed because the spec bore no correlation to user needs?

DawkinsGawd 11y ago

I always thought that correctness (in computer science) only asserted that an algorithm acted as specified. For example, say the specification was: The input accepts an element in the set of real numbers, and the corresponding output is that number added to the next element in the set of natural numbers. If this algorithm is used to dispense some type of medication, and I enter 3.1 and it murders you with 10 grams of alprazolam... well.... the algorithm is still correct.

seanwilson 11y ago
> I always thought that correctness (in computer science) only asserted that an algorithm acted as specified. For example, say the specification was: The input accepts an element in the set of real numbers, and the corresponding output is that number added to the next element in the set of natural numbers. Nobody is saying the formal proof approach will find all bugs, just that it helps find more bugs compared to not using it. You could make the same argument with acceptance testing: unless you specifically tried 3.1 as the input during testing, it might not give you the output you expect. Formal proof can be complimentary to traditional automated tests and QA.

taneq 11y ago

I've always parsed this quote as "Beware of bugs in the above code; I have only proved that the code is correct, I haven't actually compiled and tested it." For any non-trivial code, no matter how much formal analysis you do, you don't trust it until it's been properly tested.