I'm going to reply to my own comment to make a digression.
It's an intuitionistic logic theorem that the excluded middle is "irrefutable", that is, that you can never exhibit a counterexample. You can prove this constructively! This leads to something called the double negation translation, where all theorems that could be proved using excluded middle can be proven constructively to be "irrefutable" (rather than "true"), that is, that it would be impossible for an exception or counterexample to the theorem to exist. So you will get ~~P where classical logic could establish P (and deducing P from ~~P is equivalent to excluded middle).
One argument for not assuming excluded middle in proofs is then that the deductive system automatically shows you exactly which conclusions are constructive and which are not constructive, and you can interpret your deductive system in such a way that you're getting the same answers, just with this additional information or metadata about whether the answer was obtained constructively or nonconstructively. If you prove P, you did it constructively (you can exhibit the objects that P talks about, or extract an algorithm for locating or identifying them); if you prove ~~P, you did it nonconstructively, if "it" is considered as "proving P itself" (your argument shows that it would be impossible for the objects in question definitively not to exist, but you don't necessarily know how to find or calculate them).
So one can say, again, that in working this way you're learning the same stuff about your underlying subject matter, but with additional information attached at the end!
It's an intuitionistic logic theorem that the excluded middle is "irrefutable", that is, that you can never exhibit a counterexample. You can prove this constructively! This leads to something called the double negation translation, where all theorems that could be proved using excluded middle can be proven constructively to be "irrefutable" (rather than "true"), that is, that it would be impossible for an exception or counterexample to the theorem to exist. So you will get ~~P where classical logic could establish P (and deducing P from ~~P is equivalent to excluded middle).
One argument for not assuming excluded middle in proofs is then that the deductive system automatically shows you exactly which conclusions are constructive and which are not constructive, and you can interpret your deductive system in such a way that you're getting the same answers, just with this additional information or metadata about whether the answer was obtained constructively or nonconstructively. If you prove P, you did it constructively (you can exhibit the objects that P talks about, or extract an algorithm for locating or identifying them); if you prove ~~P, you did it nonconstructively, if "it" is considered as "proving P itself" (your argument shows that it would be impossible for the objects in question definitively not to exist, but you don't necessarily know how to find or calculate them).
So one can say, again, that in working this way you're learning the same stuff about your underlying subject matter, but with additional information attached at the end!
This is described in a more formal way at
https://en.wikipedia.org/wiki/Double-negation_translation