At a very broad philosophical level---which is something one must assume if you're going to talk foundations of mathematics---"formalistic" logic makes a really

At a very broad philosophical level---which is something one must assume if you're going to talk foundations of mathematics---"formalistic" logic makes a really unbelievable assumption: All facts are either true or false. Gödel of course blew this idea up quite elegantly, but the thrust of the idea is encoded directly into classical logic: (P \/ not P) is saying exactly that. Intuitionistic logic is a development of constructive logic which takes seriously the idea that many statements are at least presently unknown and possibly unknowble. Taking this very seriously we find that we cannot even use three-valued logic like "True | False | Uncertain", but instead require a logical valuation with infinitely many states. In practice, it's super convenient to use classical logic. You can use proof by contradiction, e.g. On the other hand, you have to deal with some idealogical uneasiness when you think really hard about graphs, real numbers, or the Axiom of Choice. In practice, we cannot imagine the world bereft of some of the theorems which require these uneasy choices. Simultaneously, AoC, for instance, allows bizarre obviously alien results like Banach-Tarski. Constructive logics and especially intuitionistic logics are an attempt to get past this and use a language which has the same force without the aliens and misfits. Unfortunately, the result is something that is more complex to wield.