[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.