The issue of *purity* in Haskell and this thread has confused me. At value level (not type level) is this linked with *equational reasoning*? Are the operational semantics of Haskell similar but not the same as equational logic? Why are theorem provers such as Haskabelle need? http://www.mail-archive.com/haskell-cafe@haskell.org/msg64843.html Pat