mapM

It's funny that the .gitignore is marked as being from 49 years ago ...

I think you misunderstand. On your point about programs not being "provable": it is certainly possible to prove some properties about some programs. It is not necessarily easy, and it very much depends on the program and the property in question, but it is possible.

However, this is not what the article is about. Instead, it talks about an interesting observation that there is a direct correspondence between a certain kind of program and a mathematical proof, and also between the type of the program, and the theorem validated by the proof. In other words, you can think of mathematical proofs as computational objects. The intuition for the correspondence is not hard: for example, support I want to prove that "if A is true, then B must also be true". You may think of a proof for such a property as a program, which takes as input a proof that `A` holds, and as its output produces a proof that `B` holds.

You can use monads to track where effects are used, and scope them. This allows you to write pure functions that uses effects in their implementation, but the users of the function need not worry about that.

Some monads are also handy for structuring certain kind of code---for example, the non-determinism monad can be handy for writing searches, etc.