Law of Excluded Middle Controversy

I was reading an introductory book on logic and it mentioned in passing that the Law of Excluded Middle is somewhat controversial. I looked into this and what I got was the intuistionists did not accept it in contrasts to the formalists. I'm curious but I'm only taking an introductory course in logic though very informally and vaguely I do know the history of mathematics upto Godel's incompleteness and Hilbert's program.

Can anyone tell me what is the nature of the controversy in a way that suits my level of understanding about mathematics? Further, what is an example of constructive mathematics or constructive mathematical proof and why do the intuistionists say that LEM is no good for it(if that's right)? Thanks!

Basically, the "issue" is, that with LEM you can "decide" things that a machine or (a person) could never decide on their own.

Pick two random reals $a,b$. Then obviously $a<b, a>b$ or $a=b$, right? But if $a=b$, how would you ever know that? You start comparing the digits of $a$ and $b$ and find that they are all the same, but you can never know for sure, because the sequences of digits are infinite. Hence, the program comparing two numbers would never halt, if they are the same.

That is the basic idea of constructive mathematics: If a program can't decide, then it is simply undecidable. And so, it is constructively not a theorem, that for all reals $a,b$ we have $a<b, a>b$ or $a=b$.

Another issue is, that in the same fashion for any property $\phi$, there is an $x$ with $\phi(x)$ or there is no $x$ with $\phi(x)$, according to LEM. But this makes no sense constructively: "there exists" means "I can find one", but for example: Given a continuous function $f : [a,b] \to \mathbb{R}$ with $f(a) < 0$ and $f(b)>0$, you know that, classically, there is an $\xi$ with $f(\xi) = 0$, but you cannot necessarily find that exact $\xi$, you can only approximate it. This is why this theorem fails constructively (but it works if you only claim that a zero can be approximated)

I should mention: the axiom of choice implies the non-constructive existence of various objects, so it should come as no surprise, that it implies LEM in constructive mathematics (Diaconescu's theorem).

The law of excluded middle (LEM) is the crucial ingredient in any proof by contradiction (as opposed to proof of contrapositive). The objection to LEM is most easily understood in this context.

Some proofs by contradiction establish the existence of this or that mathematical object. Constructively speaking, the problem with a proof by contradiction is that it does not provide any indication of how such a mathematical object is to be found or described specifically.

Briefly put, the constructivist claim is that existence is construction, rather than proof of impossibility of nonexistence.

The constructive mindset leads one quite far afield and leads to startling conclusions, such as the idea that the traditional extreme value theorem could be false constructively.

To understand this concept intuitively, notice that there is no way to find an approximation to such a claimed extremum. This is because the extremum is not a continuous function of the input function, as one easily convinces onself by looking at simple examples of a function with two "humps" of about the same height.