12 Feb 23:47 2013

## Why isn't "Program Derivation" a first class citizen?

Nehal Patel <nehal.alum <at> gmail.com>

2013-02-12 22:47:12 GMT

2013-02-12 22:47:12 GMT

A few months ago I took the Haskell plunge, and all goes well... -- but I really want to understand the paradigms as fully as possible, and as it stands, I find myself with three or four questions for which I've yet to find suitable answers. I've picked one to ask the cafe -- like my other questions, it's somewhat amorphous and ill posed -- so much thanks in advance for any thoughts and comments! ---- Why isn't "Program Derivation" a first class citizen? --- (Hopefully the term "program derivation" is commonly understood? I mean it in the sense usually used to describe the main motif of Bird's "The Algebra of Programming." Others seem to use it as well...) For me, it has come to mean solving problems in roughly the following way 1) Defining the important functions and data types in a pedantic way so that the semantics are clear as possible to a human, but possibly "inefficient" (I use quotes because one of my other questions is about whether it is really possible to reason effectively about program performance in ghc/Haskell…) 2) Work out some proofs of various properties of your functions and data types 3) Use the results from step 2 to provide an alternate implementation with provably same semantics but possibly much better performance. To me it seems that so much of Haskell's design is dedicated to making steps 1-3 possible, and those steps represent for me (and I imagine many others) the thing that makes Haskell (and it cousins) so beautiful. And so my question is, that in 2013, why isn't this process a full fledged part of the language? I imagine I just don't know what I'm talking about, so correct me if I'm wrong, but this is how I understand the workflow used in practice with program derivation: 1) state the problem pedantically in code, 2) work out a bunch of proofs with pen and paper, 3) and then translate that back into code, perhaps leaving you with function_v1, function_v2, function_v3, etc -- that seems fine for 1998, but why is it still being done this way?(Continue reading)