[Haskell-cafe] Haskell.org GSoC
Daniel Kraft
d at domob.eu
Thu Feb 19 02:18:21 EST 2009
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
More information about the Haskell-Cafe
mailing list