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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
