[librexpr]

In addition to this, I'd like to add that intuitionistic logic is consistent if and only if classical logic is. This follows from the Godel-Gentzen negative translation[0], which implies that for any contradiction in classical logic, you can get the same contradiction in intuitionistic logic more or less by adding "not not" before both sides of the contradiction. The same applies to the axiom of choice: set theory with choice is consistent if and only if set theory without choice is consistent[1].

This means that you don't get any safety by rejecting the law of excluded middle, nor by rejecting the axiom of choice. For this reason, I think intuitionistic logic is trading away a lot of power for basically no gain.

[0] https://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_neg...

[1] https://en.wikipedia.org/wiki/Axiom_of_choice#Independence