There are number of proof verification systems that do not require constructive logic. So if you require classical logic, just use a tool that supports it.
That's irrelevant, all mainstream proof assistants are compatible with classical logic.
That doesn't sound right at all. Law of excluded middle is very easily computed with, It's a college homework exercise.
Well, yes because you can embed classical logic in constructive logic in many ways but then you lose a lot of convenience.
The if you had exensionality things get really weird