You are also going to encounter other funny things. One of De Morgan’s laws failing could seem troubling but ultimately theoretical—how, then, about the distinction about countable and constructively countable[3]? The set of all programs is countable; the set of all terminating programs is a subset of it, but can’t constructively be proven to itself be countable—after all, that would imply a solution to the halting problem! (Neither can it constructively be proven to not be such, as it is such in a consistent extension, namely classical mathematics.) Thus you get the new and exciting notion of subcountable sets. And that’s one of the mildest things that you’re going to encounter in your shiny new theory of cardinals.
(Anybody who can explain to me what the hell constructive Hahn—Banach[4] is about gets a beverage of their choice if we are ever in the same city. Without HB, you cannot do any functional analysis worth a damn, and without that you can’t really talk about Green’s functions / fundamental solutions to linear PDEs, which are in turn a basic tool for any electodynamics or quantum mechanics worth speaking about. Unless you want to forgo proof or the natural sciences, you need it, is my point.)
None of this is to say that I think intuitionistic logic is useless, mind you. It’s interesting and useful[5]! But so far it seems that you need to learn at least some logic (as a piece of mathematics and not mere terminology, so including scary words like “metalogic”) before you can really understand how it comes together.
[1] It seems categorical logic[2] says useful things about what the One True Definition should be? But I don’t understand it well enough to tell, and in any case the constructivist tradition predates not only it but category theory in general.
[2] https://mikeshulman.github.io/catlog/catlog.pdf
[3] https://ncatlab.org/nlab/show/constructive+mathematics
[4] https://www.cse.chalmers.se/~coquand/hahn1.pdf
[5] https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016...