<div dir="ltr"><div style="font-size:12.8px">Hello all,</div><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">I'm happy to announce the first public release of sbvPlugin, a new GHC-core plugin based on the SBV library: <a href="http://hackage.haskell.org/package/sbvPlugin" target="_blank" style="font-size:12.8px">http://hackage.haskell.org/package/sbvPlugin</a></div><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">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:</div><div style="font-size:12.8px"><br></div><div style="font-size:12.8px"><div style="font-size:12.8px">    {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}</div><div style="font-size:12.8px">    module Test where</div><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">    import Data.SBV.Plugin</div><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">    {-# ANN test theorem #-}</div><div style="font-size:12.8px">    test :: Integer -> Integer -> Bool</div><div style="font-size:12.8px">    test x y = x + y >= x - y</div><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">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: <a href="http://github.com/Z3Prover/z3">http://github.com/Z3Prover/z3</a>)</div></div><div style="font-size:12.8px"><a href="http://github.com/Z3Prover/z3"><br><br></a></div><div style="font-size:12.8px">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.)</div><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">  <a href="http://hackage.haskell.org/package/sbvPlugin/docs/Data-SBV-Plugin-Examples-MicroController.html" target="_blank">http://hackage.haskell.org/package/sbvPlugin/docs/Data-SBV-Plugin-Examples-MicroController.html</a></div><div style="font-size:12.8px"><span style="font-size:12.8px"><br></span></div><div style="font-size:12.8px"><span style="font-size:12.8px">The sbvPlugin takes advantage of the SBV library (</span><a href="http://hackage.haskell.org/package/sbv" style="font-size:12.8px">http://hackage.haskell.org/package/sbv</a><span style="font-size:12.8px">) 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.</span><br></div><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">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.</div><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">The plugin is still in its early days, and there are a number of rough edges. Any feedback is most welcome!</div><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">Happy hacking,</div><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">-Levent.</div></div>