A lot of responses are going to say something like "it is mathematics without using the law of the excluded middle, or proof by contradiction" or something like that. They are not technically wrong, but I'd like to offer a different perspective.

The constructive logic used in constructive mathematics is classical logic with two new connectives added: the constructive existential, and the constructive disjunction (which could be defined in terms of the constructive existential).

The constructive disjunction and constructive existential connective has semantics given by the BKH interpretation[1]. A proof of the constructive disjunction A + B is either a proof of A or a proof of B. A proof of the constructive existential Σn:N. P(n) is a pair <n,p> where n is a natural number and p is a proof of P(n).

So constructive mathematics isn't classical mathematics hindered, but constructive mathematics is mathematics enhanced with a more expressive language. Naturally constructive mathematics tends to focus on theorems written in this more expressive language that make use of these new constructive connectives, rather than focusing on the classical fragment which is already well studied.

For the non-layman: we can see that the above interpretation is correct because the fundamental logical rules for universal quantification, implication, conjunction, false and true are all identical between classical and constructive logic. And, according to classical mathematicians at least, this set of logical combinatorics is complete. Thus the law of excluded middle holds, even in constructive logic, so long as you use the classical disjunction, which is defined in terms of conjunction, implication, and false. Similarly you can prove that proof by contraction, i.e. double negation elimination ¬ ¬A -> A is a theorem of constructive logic whenever A is a formula that does not use the constructive disjunction or constructive existential (where negation is defined in terms of implication and false).

For the all of the above, I'm particularly focused on first-order number theory, however all of the above carries over to higher-order theories, and I think it even holds for set theory (or at least some large part of set theory such as Zermelo set theory; I forget what happens with the replacement axiom). Higher-order constructive mathematics does come with the caveat that the Axiom of Choice is not a theorem of constructive mathematics even when it is phrased only using the classical existential.

[1]https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%...