Hi, Am Dienstag, den 12.02.2013, 17:47 -0500 schrieb Nehal Patel:
To me, it seems that something like this should be possible -- am i being naive? does it already exist? have people tried and given up? is it just around the corner? can you help me make sense of all of this?
a related project is HOLCF-Prelude, by Christian Sternagel and others. What they do is to reimplement the Haskell prelude as HOLCF data types and functions in the theorem prover Isabelle. This allows you to write functional code as HOLCF functions, prove properties of them (using functions from the prelude and a library of lemmas about them) and, as long as the definitions are the same as in your Haskell code, be happy about it. It is not a silver bullet, and not exactly what you need. For example, you still have to manually translate between the HOLCF definition and the Haskell code. Also, Haskell is not covered completely. Exceptions, for example, are completely ignored. But nevertheless it is useful: For example, we have started to verify some of the transformations suggested by hlint, proved quite a few of them and even found (very few) wrong ones. And what wren said about the complexity of machine verified proofs is very true. Especially when you also cover non-termination and lazyness (as we do) and want to prove properties involving type classes with a few assumptions about them as possible, and suddenly have the problem that (==) can do arbitrary stuff. You can find the code at https://sourceforge.net/p/holcf-prelude/ Comments and contributions are welcome! Greetings, Joachim -- Joachim "nomeata" Breitner Debian Developer nomeata@debian.org | ICQ# 74513189 | GPG-Keyid: 4743206C JID: nomeata@joachim-breitner.de | http://people.debian.org/~nomeata