> vehicle for doing mathematics with intuitionistic logic, and in particular denying the law of excluded middle

I think this is the basis for the enthusiasm, almost entirely. There's a growing perception that a lot of mathematical abstractions that are purely naval-gazing have arisen from ZFC, and the intuitionalists and finitists are gaining followers amongst amateur and upcoming mathematicians. I don't have data to back this, just a feeling that I get.

And I think in particular this is attractive to programmers because this skews closer to what we've learned about computability and program design, and I think there's even some hope of moving forward from obscure notation and single-letter variable names towards a syntax for doing mathematics that can be more expressive and easier to verify.