Good question! I believe I have the solution for this, actually. I am just working out the foundations properly (I call it "Abstraction Logic"), but the basic direction of it is described at https://practal.com
But what is "this"? I think the only criticism of existing theorem provers at https://practal.com is that Coq uses coercions rather than subtyping. Is there a practical example where Coq just doesn't have a good equivalent for what subtypes can do?
Coercions / subtyping is a big one, because mathematics is full of quotient types and identifications. This is a very practical issue, that comes up many many times. Not necessarily if you "program" in Coq, but if you try to do math in Coq. Another one is that there is no good treatment of undefinedness. An "option" type doesn't cut it, because it pollutes everything. The question is, how can you enable undefinedness everywhere, without polluting everything? That is only possible by adjusting your logic.
What foundation would you rather have?
And what would it do better / how would it be less "detrimental" to formal mathematics?