Correctness

In theoretical computer science, correctness of an algorithm is asserted when it is said that the algorithm will certainly terminate, and the answer returned will be correct. This contrasts in particular with an assertion of partial correctness, to the effect that if an answer is returned it will be correct. Since there is no general solution to the halting problem, a correctness assertion may lie much deeper. For example if we are successively searching though integers 1, 2, 3, ... to see if we can find an example of some phenomenon - say an odd perfect number - it is quite easy to write a partially correct program (use integer factorization to check n as perfect or not). To say the program is correct is to assert something currently not known in number theory.

A correctness assertion is therefore relative to a given algorithm and a specification. A proof would have to be a mathematical proof, assuming both of those things given formally. In particular it is not expected to be a correctness assertion for a given program implementing the algorithm on a given machine. That would involve such considerations as limitations on memory.