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