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". _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe