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