A term describing a relation: a program is said to be correct with respect to some specification if it fulfills all the constraints of this specification.

That is, a program is correct if it would do what it should in all the contexts where you would consider it. Of course "what it should" and "the contexts where you would consider it" are relative concepts that depend on the specification.

Every programmer strives to write correct programs.

Since the beginning of theory of computation, before even computer were born, people have reasoned about programs; practical tools, techniques and methods to design correct programs have been developed: program state inspectors, debuggers, safer languages, development methods, etc. But all these are tradesmen's make-shift solutions. Cleaner languages exist, with well-defined mathematical meta-languages suitable for expressing the properties of programs, but only recently has automated verification of program correctness become a technique suitable for use in large-scale industrial software.

Also see Bug, Proof, Security, Specification, Verification.

This page is linked from: Functional