[Gondolin]

Oh yes, it is very much alive. For instance any topos (with a nno) is a model of intuitionist set theory. And since topos are a very natural type of categories (a topos= acategory which has finite limits and a power object), intuitionist logic is important in category theory.

Two examples: in algebraic geometry, mathematicians use schemes (introduced by Grothendieck), which have allowed to make tremendous progress. But from the point of view of intuitionist logic, a scheme is just a ring, and a quasi-coherent sheave is just a module over this ring (in more details they are ring objects and module objects in the big Zariski topos).

In synthetic differential geometry, one use a certain intuitionist topos to formalize intuitive aspects of reasoning with infinitesimal quantities (without relying on delta and epsilons). Note that non standard analysis also allows to work with infinitemismal quantities (by using ultraproducts), but has the same power has standard analysis (and in particular is classical). Synthetic differential geometry is intuitionnist, so is less powerful, but on the other hands its theorems are automatically valid for more models (complex models, formal smooth schemes...). In SDG, your reals R are a field with an (actually several) element epsilon !=0 (the infinitesimals) and such that epsilon^2=0 (that's why this only work in intuitionist logic, in classical logic R being a field would imply that epsilon=0). In this model every function f: R->R is differentiable, and we have f(x+epsilon)=f(x)+f'(x) epsilon.

In proof theory (like coq) one work with Martin Lof type theory, which is the type theory of topoi (and so is intuitionist). A recent development is to work with homotopy type theory instead, the type theory of \infty-topos. This is more powerful (and can be used as fundations for all of maths), and solve real problems, like correctly defining equality (equality is actually a tricky concept, for instance it may not be the case in the prover's theory that "for any two functions f and g such that forall x, f(x)=g(x); then f=g", but this is obviously a feature we want.) On the other hand it is quite a bit trickier to define (we need (infty,1)-categories).

[Gondolin]

On the other hand, constructive set theory is still rather a niche part of mathematics (this may change with the recent development of HOTT). It is hard not to use the LEM (and I am not good at it, I am not an expert on this subject. Expert say it gets easier over time to get used to not use LEM).

For instance, in the intuitionist reals, from "x >= 0 and x != 0" you cannot conclude that "x != 0". To prove x>0 you would need to exhibit a natural number n such that x>=1/n (so in other words you need a constructive proof that x>0). But this is not always possible, you have models of R where there is an x != 0 which is smaller than all the 1/n.

There is however one nice feature of intuitionist theory: every geometric sentence which is provable in classical theory is actually true in intuitionist theory. So if you have a geometric sentence (https://ncatlab.org/nlab/show/geometric+theory) you can use LEM in your proofs, the proof will still be valid intuitionally!