[Haskell-cafe] Formal Program verification in Meta-Haskell

[Alexander McPhail]

Hi,

I have no understanding of template haskell and thus this message is
uninformed speculation.  Would it not be possible to write a function
verifier in TH that, unlike QuickCheck which provides bounds on a function
being probably approximately correct, is given a list over properties which
are proven over a quasi-quoted syntax tree?

For example:

> multiply :: Num a => a -> a -> a

> multiply_group :: Proof Bool
> multiply_group = group multiply 1

> group :: (a -> a -> a) -> a -> Proof Bool
> group f ident = [proof| f, [associative, identity 1]]

where `associative` and `ident` are proof-constructing functions that act
over the `f` syntax tree.  (Maybe some invokation of an Isabelle-like
theorem prover or an SMT-like solver as part of the 'proof' module).

Then we might even be able to list properties with class declarations.  The
properties get verified at compile time.

> class Monoid a where
>   mzero :: a
>   msum :: a -> a -> a

>   property a [associative msum, identity mzero msum]

Any thoughts?

Vivian
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110120/9beb4f17/attachment.htm>