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

On Sat, Jun 5, 2010 at 8:10 PM, Thomas Hartman 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