One other way to prove these algorithms is by writing them in z3 prover. You write a simple one that is 100% correct and then you prove equality for your optimized one or find an example that will show inequality.
I'm only familiar with using "unary" to mean single-parameter.
And the etymology is basically a coincidence because "mono" got used in different places, isn't it?
Actually, all monads are monadic functions/operators on their (usually type) parameter. Eg, 'list' is a monadic operator from element types to types of lists of those elements.
It's completely different (AFAICT), and mostly unrelated, but it's not completely unrelated.