[Haskell-cafe] Merging SMT solving and programming languages: two EDSLs for SMT in Haskell

[Don Stewart]

Hey all,

For a while now, Galois has been interested in connecting automated solvers to
our programming language of choice, Haskell, to make it possible to prove
automatically some properties of our functions (rather than just testing, e.g.
with QuickCheck). We've pushed two efforts out this week, as previews of what
we're thinking in this space:

 * SBV; and
    http://hackage.haskell.org/package/sbv

 * yices-painless.
    http://hackage.haskell.org/package/yices-painless

Both are embedded DSLs for representing propositions to an SMT solver via
Haskell functions and values. They take different approaches (a compiler from
Haskell to the SMT-LIB format, versus an interpreter for the Yices SMT solver).
SBV is the more mature package, while yices-painless emphasizes a
type-preserving translation from a minimal core language. SBV was built by
Levent Erkok, yices-painless by Don Stewart. Documentation for the design of
yices-painless is available, as is documentation on SBV.

Both are ready for experimentation and feedback, and we welcome your comments.

More information is on the blog:

    http://corp.galois.com/blog/2011/1/18/merging-smt-solvers-and-programming-languages.html

-- Don