Yes. But "background logic" (which classical first-order logic strives to model) is needed to prove meta theorems about any of the constructive logics. While

Yes. But "background logic" (which classical first-order logic strives to model) is needed to prove meta theorems about any of the constructive logics. While the object-level proofs in some constructive/intuitionistic logic might do away with the law of excluded middle, the meta-theoretics proofs (proofs of theorems about the formalism) usually use them quite freely. My point is that there is no formalism that can ignore LEM at all levels (informal --> meta-theoretical--> object). The constructive logics are quite useful for things like program generation but I am not sure if we should use them as a model for human reasoning.