[Haskell-cafe] [ANNOUNCE] sbvPlugin: Run SMT solvers over Haskell "theorems"

[Levent Erkok]

Hello all,

I'm happy to announce the first public release of sbvPlugin, a new GHC-core
plugin based on the SBV library:
http://hackage.haskell.org/package/sbvPlugin

The plugin can be used to prove (or refute!) theorems in your Haskell code,
using the SBV library as its backend. Here's a most simple example:

    {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}
    module Test where

    import Data.SBV.Plugin

    {-# ANN test theorem #-}
    test :: Integer -> Integer -> Bool
    test x y = x + y >= x - y

When compiled (or loaded into ghci), you'll see that the plugin will
attempt to prove the given theorem, and will produce a counter-example
since it is not valid! (This assumes, you've installed an SBV-supported SMT
solver. Z3 from Microsoft is a good choice: http://github.com/Z3Prover/z3)


<http://github.com/Z3Prover/z3>
The plugin is still in its early days and the examples are rather sparse.
But see the following for one worked out instance: (Thanks to Anthony
Cowley for the original idea.)


http://hackage.haskell.org/package/sbvPlugin/docs/Data-SBV-Plugin-Examples-MicroController.html

The sbvPlugin takes advantage of the SBV library (
http://hackage.haskell.org/package/sbv) to directly reason about Haskell
programs at GHC's core level. However, the plugin is *not* a replacement
for SBV. It only exposes a few features of SBV directly at the Haskell
level; which hopefully makes it useful and more friendly than SBV; but it
is neither intended nor possible for it to replace the SBV library itself.

In particular, the plugin is limited to certain types (mostly numeric), and
a few composite ones (lists and tuples.) If the plugin does not
"understand" a Haskell type/expression, it'll use a technique called
"uninterpretation" to black-box it. In those cases, the counter-examples
produced might be bogus, though proofs will still be valid. Note that any
definitions that are outside of the module being compiled will also go
uninterpreted, including all the Prelude functions.

The plugin is still in its early days, and there are a number of rough
edges. Any feedback is most welcome!

Happy hacking,

-Levent.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20151222/3b3f0e6f/attachment.html>