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.
Cheers
Peter White, Motorola
