Non-deterministic monad: a bit of formalism