[Haskell-cafe] is there a way to prove the equivalence of these two implementations of (Prelude) break function?

[Jason Dagit]

On Sat, Jun 5, 2010 at 8:10 PM, Thomas Hartman <tphyahoo at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100607/2b1c31d8/attachment.html