[DawkinsGawd]

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]

> 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.