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 craftworkmen make-do's cleaner languages, with a well-defined mathematical meaning meta-languages where to express 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).
