> Idea 1:
> Export Haskell declarations to a theorem prover, such as HOL
> or PVS. Then
> permit the user of the theorem prover to state and prove
> properties of the
> Haskell program, using the exported definitions.
>
> Ideas 2:
>
> There was recently a discussion about adding "rules" to
> Haskell, that document
> the properties that are desired from a class. How about adding such
> annotations (perhaps as some kind of special comment syntax). These
> additions would be without any semantic content *to Haskell*. However,
> the rules could also be exported to HOL, PVS, ..., so that a theorem
> prover could be used to discharge these proof obligations.
Good ideas.
Indeed the RULES that I've added to GHC (in the CVS tree but not
in a 4.xx release yet) take exactly this form:
{-# RULES
"app1" forall xs . xs ++ [] = xs
#-}
What I have not done (any volunteers) is to export these rules, or
the function definitions to a thm prover.
Simon
