[jmillikin]

That's a frankly silly position to hold.

There's no reason to avoid ST, and in many cases it makes the code clearer and shorter than trying to figure out some pointfree contortionism to reach the same goal.

I'll look at Coq when it has support for binding to C libraries, opening sockets, or doing anything else than a programming language needs to support.

[eurleif]

You seem to be setting up a false dichotomy between using the ST monad and writing pointfree code ("functions as a composition of other functions, never mentioning the actual arguments they will be applied to"). But you can write non-pointfree code that doesn't use the ST monad, and you can write pointfree that does use it. They're unrelated.

[Locke1689]

ST is just a prettified C that's safe and well-typed. If you want to write C in Haskell that's fine, but you're not doing functional programming.

This is always the user/theorist divide. I'm not saying that sometimes ST isn't necessary, but it should always be the smallest necessary imperative subset.

By the way, the authors of the ST monad make this same point (read the paper). ST is (by necessity) always single threaded. It ruins modularity by not being able to interact with any non-ST code. In short, it's not functional.

Anyway, theorists will continue to do interesting things with Coq and whether or you think it's sufficient as a "programming language," it's useful to us.