Monads as a concept is basically just a fancy version of a wrapper class (if you in OOP land). Do we really need the cognitive overhead of advanced mathematics to explain that?
If you want to limit yourself and make sure people keep reinventing the same concepts over and over, sure, avoid maths.
In particular, the dichotomy you created which paints the two options as “advanced mathematics” and “intuition” seems to need some proof that there is no third option. Since the original poster mentioned OOP, that would be a good place to start with some example of a problem which is hard to avoid following good OOP practice.
In programming you end up with JavaScript Promises instead of proper monads because of similar appeals to intuition. A monad obeys certain laws upon which further abstractions can be built. Promises do not obey those laws and so one cannot benefit from them. A programmer has to learn what a Promise is and how it behaves. You learn what a monad is once and anything that is a monad behaves the same way.
The reason why it’s important to use the proper names is so that people can find the original definitions and theorems. You don’t have to be a category theorist to use a monad. You can have a basic understanding, as I do, and get by fine. However when you want to understand the theorems to build your own abstractions it’s great being able to go straight to the source.
Simon Peyton-Jones has a good explanation for why Haskell took this route in his talk, Escaping the Ivory Tower.
My contention is not that writing things down or naming abstractions is bad. On the contrary i think that is a good thing.
I don't even think monads are a bad abstraction. Monads are a fine abstraction. Its the baggage people carry with it that is the problem.
My main contention is that people are cargo culting the way monads are explained in category theory and applying that to computer programming. This sort of works, but generally not that well because its copied from a field with very different goals.
Math wants to prove things in the most general way possible. This lets them explain & discover the deepest possible patterns. They trade complexity to achieve this goal.
Computer programming aims to solve problems efficiently in a way that is efficient and easy to modify. Complexity is the enemy of this goal.
Even in math, you might prove that some object is a monad or whatever, but you will still generally work from its normal definition and not from the definition of a monad.
The language of category theory is great for proving things. Its esecially great for proving things in very general ways.
Computer programming (to be clear: different from computer science) is not math. Sure programs are proofs (/me waves at howard-curry) but they are not the types of proofs math is generally interested in. Its the same task applied to different goals. The tools for both might work in both contexts, but they are not going to work equally as well.
That's not to say we shouldn't try and formalize things - we should. Category theory is just not a good design pattern language for typical programming tasks. It wasn't designed with that goal in mind, it does a bad job with it. Worse, it sounds very learned, so pseudo-intellectuals use it to gate-keep.
You don’t have to be a gatekeeping, academic elitist to understand how to use a monad. I use them every day at work and I program on my stream where I’m using them all the time.
What’s nice about it is that if I want to go on that journey and learn more about monads so that I can build my own abstractions upon them I can go right to the source definitions.
I don’t have to go look up what a BurritoWrapper is and all of the methods designed for it that only work with whatever the author designed them for. Once I know I have a monad I know how to use it.
Curry-Howard is super cool and we should formalize things more.
For a common example of this phenomenon- I took a look into the innards of printf to see how printf("%f",...) and printf("%g",...) works. I am still clueless how it actually works. Does not prevent even beginners from using these.
==
Also for what it is worth, I think the most useful analogy of monads is "monads are pipes with types", even though it does not give a full understanding of bind.