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

[Joachim Breitner]

Hi,

Am Dienstag, den 12.02.2013, 17:47 -0500 schrieb Nehal Patel:
> 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?

a related project is HOLCF-Prelude, by Christian Sternagel and others.
What they do is to reimplement the Haskell prelude as HOLCF data types
and functions in the theorem prover Isabelle. This allows you to write
functional code as HOLCF functions, prove properties of them (using
functions from the prelude and a library of lemmas about them) and, as
long as the definitions are the same as in your Haskell code, be happy
about it.

It is not a silver bullet, and not exactly what you need. For example,
you still have to manually translate between the HOLCF definition and
the Haskell code. Also, Haskell is not covered completely. Exceptions,
for example, are completely ignored.

But nevertheless it is useful: For example, we have started to verify
some of the transformations suggested by hlint, proved quite a few of
them and even found (very few) wrong ones.

And what wren said about the complexity of machine verified proofs is
very true. Especially when you also cover non-termination and lazyness
(as we do) and want to prove properties involving type classes with a
few assumptions about them as possible, and suddenly have the problem
that (==) can do arbitrary stuff.

You can find the code at https://sourceforge.net/p/holcf-prelude/
Comments and contributions are welcome!

Greetings,
Joachim

-- 
Joachim "nomeata" Breitner
Debian Developer
  nomeata at debian.org | ICQ# 74513189 | GPG-Keyid: 4743206C
  JID: nomeata at joachim-breitner.de | http://people.debian.org/~nomeata

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130214/48688cd5/attachment.pgp>