# Are functional languages a kind of program derivation?

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?

Haskell code can certainly be read as a description of how to perform the computation (the STG machine is basically a stripped-down, more explicit Haskell-style functional language but has direct, obvious execution semantics). But yes, the more common reading is a declarative one, and declarative programming is closer to formal specifications than imperative languages.

However, you'd have to stretch the definitions of program derivation to include functional programming in it. For one, if you call any kind of transformation from a language into machine code, then even a C compiler is a program derivation tool. Second, (most) functional languages are in no sense specification languages: Code is written to make obvious what is being computed rather than how, but it still spells out the computation (although it does this in different terms than, say, C, and perhaps leaves more room for compiler optimizations) rather than letting the compiler search for a program. The distinctions are blurry, but people tend to draw the line somewhere between Haskell and full-on propositional logic.

To derive a program means to write a formal specification, which is usually non-executable, and then apply mathematically correct rules in order to obtain an executable program satisfying that specification. That describes a compiler, basically.

Haskell is a programming language that uses mathematical rules to help you verify program correctness. It is a tool that helps you derive a program. You still have to perform the derivation process, within the confines of the programming language.

The notion that you are describing what things are, rather than how the computation is done, is what declarative vs. imperative programming means. Imperative programming is programming in the small, by specifying a recipe; a series of steps. Declarative programming is where you essentially tell the computer what you want, and it figures out how to get it done.

Declarative programming is characterized by referential transparency, mathematical correctness, the lack of side effects, laziness and concurrency; all of the things that Haskell excels in.

If it's possible to algorithmically generate imperative machine code from your specification, then your specification is, by definition, itself a program - most likely a Domain Specific Language.

What about the converse, is a program a specification? Part of the definition of a specification is probably that it be understandable to humans what it does and why it does it. Clearly this is pretty fuzzy. What humans, what degree of understanding? Arguably functional languages declarative nature makes them more understandable to humans, but the state of affairs today is that most programmers are more familiar with imperative languages and understand them better, so it's pretty hard to take that as a proven fact.