It's because they use metaprogramming so extensively. As an example, HOL4 (I can only speak for that) accepts a script written by the user (as though in a REPL), compiles and runs it, and produces an sml theory file which represents their defined theory [0]. The user when they start their next theory are supposed to use this computer generated code.
You would have to write your own repl, write your own way of loading, writing theories etc and by that time you've lost performance (HOL even after 20 years of progress and tweaks now has only mostly ok performance).
So it would at least require some rearchitecting, which is my point; it's not a drop in replacement.
That makes sense. It's pretty cool to think that ML was designed as a metalanguage for theorem provers, and the innovations required for that turned out to be the next step (or next several steps) in the evolution of general-purpose languages.
You would have to write your own repl, write your own way of loading, writing theories etc and by that time you've lost performance (HOL even after 20 years of progress and tweaks now has only mostly ok performance).
So it would at least require some rearchitecting, which is my point; it's not a drop in replacement.
[0] - This is AES, before and after building! https://gist.github.com/j-baker/244ef3e59f19d74c352b