Program derivation is defined as the derivation of a program from it's specifications. Usually this specification language is some form of propositional logic, but from what I understand, it need not be. For the sake of specificity, I'm only dealing with purely functional languages like Haskell here.
When you write a program in Haskell, you aren't describing how the computation is done, but what things are. For example, in this function that produces Fibonacci numbers, all this is given is a specification for Fibonacci numbers, not how the function should be implemented.
fib :: int -> int fib n = (fib n-1) + (fib n-2) fib 1 = 1 fib 0 = 1
To make this code run, the Haskell compiler must convert this declarative specification of the function to imperative machine code. Isn't this by definition a kind program derivation?