[olliesaunders]

Why wouldn’t you use it Agda/Coq for general development? (Looking for reasons other than a presumed lack of libraries.)

[Locke1689]

It's very slow and every function must have formal properties, e.g. all functions are total and must formally be proved to terminate.

(As far as I know. I've only worked through Pierce's book.)