But you are are aware of this already, I'm just writing it out.
Look at these provers, they're almost all based on classical logic, and even on proofs by contradiction:
Even Isabelle/HOL, which is quite user friendly and has a lot of automation (like Sledgehammer, which can call to the automatic provers mentioned above) is based on classical logic with choice.
But you also end up with proofs that are much, much shorter.
I guess it's all about the degree of uncertainty. Constructive mathematics reduces the degree of uncertainty, which grows exponentially as you get in the higher level proofs.