Comment by Twey

Intuitionistic logic is a refinement of classical logic, not a limitation: for every proposition you can prove in classical logic there is at least one equivalent proposition in intuitionistic logic. But when your use of LEM is tracked by the logic (in intuitionistic logic a proof by LEM can only prove ¬¬A, not A, which are not equivalent) it's a constant temptation to try to produce a constructive proof that lets you erase the sin marker.

In compsci that's actually sometimes relevant, because the programs you can extract from a ¬¬A are not the same programs you can extract from an A.