It did not take long reading that Haskell book before I got some inspiration and understood why the functional style of programming is great for writing code that can be verified with mathematical precision. Recursion lends itself to proof by mathematical induction.
I started a new project to explore this. It’s on Github at https://github.com/xerocross/xerocross.functional-util. I don’t recommend anybody else use it yet. I just publish everything to Github because it’s nice for keeping track of things.
Another part of the goal is to write these functions using recursion as the primary means of looping. The result of a recursion can be proved mathematically using proof by mathematical induction. Eventually I would like all of these utility functions to be self-proving. But it’s not always easy to figure out how to do something using recursion.