[Haskell-cafe] Haskell.org GSoC

[sylvain]

Le mercredi 11 février 2009 à 11:12 +0100, Daniel Kraft a écrit : 
> Hi,

Hi,

> Do you think something would be 
> especially nice to have and is currently missing?

In my humble opinion, Haskell presently fall short of its promises
because it does not embed theorem proving. Quickcheck-like testing is
truly great, but can not replace proofs to produce bug free software.

With use of equational reasoning + induction, one can already prove a
huge amount of useful properties of an Haskell program [1].

The idea would be to extend Haskell with a syntax to write such proofs,
and implement support for it in the GHC compiler.

This could look like:

module Integer where
  ..
  theorem read_parses_what_show_shows :
    (a :: Integer, Show a, Read a) => 
    show . read a = id a
    proof
      axiom

In the case above, programmers may resort to the "axiom" keyword, which
would at last have the merit of explicitly document assumptions. For
axioms, one would have to fall back to quickcheck and consort, so these
tools would not be made obsolete ;)

Another example:

theorem : ( xs :: [a], ys :: [a], f :: a -> b) => 
  length (map f (xs ++ ys )) = length xs + length yx
  proof
    length (map f (xs ++ ys )) =
    length (xs ++ ys) = {- use length++ -}
    length xs ++ length ys

Theorems can be named, like "length++" (which is not shown here).
Successfully proven theorems would be automatically added to the current
theorem database and could be reused in further proofs in the same
scope. 

The compiler could even be instructed to make use of this database to
optimize the program.

This theorem prover could also be used to ensure the soundness of
refinement, rewrite of an obvious version of a function/module in a more
efficient but less obvious version.

Furthermore, the compiler could be instructed to generate a "proof
obligation", which would have to be discharged by the programmer. 

instance Read Integer where
  ...

instance Show Integer where
  ...

constraint read_parses_what_show_shows where
  (Read a, Show a) => read . show a = id a

The compiler would complain if, for any couple of Read/Show instance of
the same data type, the constraint is not proved to be satisfied. 

There is more to it, of course. "Tactics" would be needed to make this
practical. Hopefully, at this stage, this project would catch interest
of the "academics", and development would take off, until we get an
almost automated theorem prover.

Haskell is a nice, mature and efficient programming language. 
By its very nature it could also become a nice executable formal
specification language, provided there is tool support. This would be
quite unique[2] and there really would be no excuse to not use it in one
step or another of the development process :)

Hope I didn't uttered nonsense.
Sylvain

PS A package even exists that may serve as basis for this work
http://www.haskell.org/haskellwiki/Haskell_Equational_Reasoning_Assistant

[1] I currently think that equational reasoning + induction is
effectively enough to prove every theorems on Haskell programs. Please
somebody knowledgeable, correct me if I am wrong?
[2] I know of "B", but it is not "nice".