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? What I'm asking about might sound related to theorem provers, -- but if so ,I feel like what I'm thinking about is not so much the very difficult problem of automated proofs or even proof assistants, but the somewhat simpler task of proof verification. Concretely, here's a possibility of how I imagine the workflow could be: ++ in code, pedantically setup the problem. ++ in code, state a theorem, and prove it -- this would require a revision to the language (Haskell 201x) and perhaps look like Isabella's ISAR -- a -structured- proof syntax that is easy for humans to construct and understand -- in particular it would possible to easily reuse previous theorems and leave out various steps. At compile time, the compiler would check that the proof was correct, or perhaps complain that it can't see how I went from step 3 to step 4, in which case I might have to add in another step (3b) to help the compiler verify the proof. ++ afterwards, I would use my new theorems to create semantically identical variants of my original functions (again this process would be integrated into the language) While I feel like theorem provers offer some aspects of this workflow (in particular with the ability to export scala or haskell code when you are done), I feel that in practice it is only useful for modeling fairly technically things like protocols and crypto stuff -- whereas if this existed within haskell proper it would find much broader use and have greater impact. I haven't fully fleshed out all the various steps of what exactly it would mean to have program derivation be a first class citizen, but I'll pause here and followup if a conversation ensues. To me, it seems that something like this should be possible -- am i being naive? does it already exist? have people tried and given up? is it just around the corner? can you help me make sense of all of this? thanks! nehal _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
