> But in the end we need to converge programming, math and logic, and once this is done, we will be ready for anything. And we won't need monads as a crutch, fo

> But in the end we need to converge programming, math and logic, and once this is done, we will be ready for anything. And we won't need monads as a crutch, forced upon us by a type system. 1. Math is filled to the brim with monads, it's just that mathematicians are necessarily specialists, and tend to think about things in terms of their applications to their specialties: they talk about closure operators or algebraic theories or formulas in a formal language, rather than monads as such. But that doesn't mean the monad structure isn't there. 2. Convergence between math and programming (which I agree is desirable) will almost certainly see type theory become more prominent, not less. There is some chance that programmers turn to constraint solvers or ML models for program verification instead, but if they do, mathematicians will not follow.