On Sat, Jun 5, 2010 at 8:10 PM, Thomas Hartman <tphya...@gmail.com> wrote:
> Here's two implementations of break, a snappy one from the prelude, > and a slow stupid stateful one. > > They are quickchecked to be identical. > > Is there a way to prove they are identical mathematically? What are > the techniques involved? Or to transform one to the other? > If you want a proof assistant, you could try using Haskabelle: http://www.cl.cam.ac.uk/research/hvg/isabelle/haskabelle.html Jason
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
