[Haskell-cafe] Haskell.org GSoC

[Daniel Kraft]

Hi,

sylvain wrote:
> 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].

this sounds like a really interesting project to me...  Especially as
I'm doing maths instead of CS as main subject (and it is simply
inherently interesting :D).

> 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

That's of course nice, but I'm at the moment not yet convinced something
like this could be more or less easily implemented also for larger
programs; and, I don't see from your example how the real implementation
of the program should play in.  Do you expect that Haskell figures out
from the implementation that (map f) does not alter a lists length?  Or
should this be an already available theorem within the Prelude?

I guess it should be the former, as otherwise the whole proofing seems
to be just documentation, without real connection to the Haskell code.
But in this case, I wonder whether something like that can be
successfully done on more sophisticated code, and especially done as
part of a GSoC project...  But I guess with a competent mentor and
clearly defined goals it should be possible.

But all in all, as stated above, this could be really interesting :)
Thanks for this suggestion and your ideas!

Daniel

-- 
Done:  Arc-Bar-Cav-Ran-Rog-Sam-Tou-Val-Wiz
To go: Hea-Kni-Mon-Pri