Program derivation is a kind of
ProgramTransformation in which an (efficient) implementation is derived from a (high-level) specification.
If the specification can be proven correct easily and the derivation preserves this correctness, it follows that the resulting implementation is correct.
Therefore, derivation is especially useful if the correctness of the final product is important and the problem it solves is very complex.
See also