[Haskell-cafe] Why isn't "Program Derivation" a first class citizen?

[Rustom Mody]

On Wed, Feb 13, 2013 at 4:17 AM, Nehal Patel <nehal.alum at gmail.com> wrote:

> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>


I am stating these things from somewhat foggy memory (dont have any
lambda-calculus texts handy) and so will welcome corrections from those who
know better…

In lambda-calculus, if reduction means beta-reduction, then equality is
decidable
Adding eta into the mix makes it undecidable
Haskell is basically a sugared beta-reducer
A prover must -- to be able to go anywhere -- be a beta-eta reducer.
Which is why a theorem-prover must be fundamentally more powerful and
correspondingly less decidable than an implemented programming language.

If a theorem-prover were as 'hands-free' as a programming language
Or if an implemented programming language could do the proving that a
theorem-prover could do, it would contradict the halting-problem/Rice
theorem.

-- 
http://www.the-magus.in
http://blog.languager.org
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130213/82409bbb/attachment.htm>