Several of my research projects involve equational reasoning on Haskell programs. Examples include the implementation of the Hydra hardware description language, formal methods for system design, parallel algorithm development, and a toolbox for discrete mathematics. In all these cases there is a need for better software tools to assist in the equational reasoning, yet the specific needs of these applications vary.

After describing a couple of the applications briefly, some preliminary ideas for a suitable toolbox will be presented.