Preliminary "terminological" note.
There are several approach to constructive mathematics: one of them is intuitionistic one.
Intuitionism was founded by Brouwer: he formulated a "kantian-like" philosophy of mathematics (regarding numbers, not geometry). His philosophy is not usually followed by mathematicians.
From intuitionism the intuitionistic logic has born: it is very interesting and widely studued today. Brouwer did not liked formalization; he was not interested in formal logic.
There are current development of constructive analysis (Bishop, Bridges, Beeson) that do not use intuitionistic logic, but the classical one.
What is the common future of those approach : the rejection of some usual methods of proof used in mathematics. First of all so-caled "non-constructive" proofs.
See Sara Negri & Jan von Plato, Structural Proof Theory (2001), page 26 :
Classical logic contains the principle of indirect proof: If ~A leads to a contradiction, A can be inferred. Axiomatically expressed, this principle is contained in the law of double negation, ~~ A => A. The law of excluded middle, A v ~ A, is a somewhat stronger way of expressing the same principle.
Under the constructive interpretation, the law of excluded middle is not an empty "tautology," but expresses the decidability of proposition A. Similarly, a direct proof of an existential proposition Exists x A consists of a proof of A for some a. Classically, we can prove existence indirectly by assuming that there is no x such that A, then deriving a contradiction, and concluding that such an x exists. Here the classical law of double negation is used for deriving Exists x A from ~~ Exists x A.
In conclusion, what all constructivists share is the rejection of the above method of proof : if I want to show that a number with a certain property P exists, I have "to show" a number n such that P(n). I'm not licensed to assert that a number with a property P exists, only when I'm able to derive a contradiction from the assumption that such a number does not exists.
You can exploit this "rejection" through intuitionistic logic, where the above rule of proof is not sound, or through a "careful" use of classical logic, i.e. avoiding this kind of proofs.
Second "terminological" note.
In order to avoid misreading I sugegst to use the description "real number line" as a definite description: the "real" must not be extrapolated and used as an adjective.
So, when we read "is the real number line real ?" we are not alluding to some "heideggerian mistery"; we are simply asking if we stay with the existence of a certain specific "kind" of numbers.
According to the constructivists, we can legitimately "speak of" only those real numbers that we are able to "construct": they are all the rationals, the algebraic ones and all the "baptized" irrationals, like SQRT(2), 3,14..., e, and so on.
A "classical" approach to constructive analysis is through "computable" numbers, i.e. all those numbers that are approximable through some algorithms (all the above are).
It is obviuos that computable numbers are countable : an algorithm is a finite set of instructions (all of which are finite strings of symbols).
Now, if we take into account Cantor's proof of the uncountability of the real, we have that no bijection exists from the natural numbers to the point in [0,1]. The classical approach conclude to the existence of uncountable many real numbers: I do not "see them" but they are "there" ...
Thus (and I beg your pardon for so long a post) the constructivist objection :
if the numbers that we may "know" (speak of, define them, name them) are countable, what kind of "reality" do have "all other" (uncountably many) (ir-)real numbers that we will never know ?
I personally appreciate the constructive manifesto of Errett Bishop, Foundations of constructive analysis (1967), page 2:
The primary concern of mathematics is number, and this means the positive integers. [...] Mathematics belongs to man, not to God. We are not interested in properties of the positive
integers that have no descriptive meaning for finite man. When a man proves a positive integer to exist, he should show how to find it. If God has mathematics of his own that needs to be done, let him do it himself.
Almost equal in importance to number are the constructions by which we ascend from number to the higher levels of mathematical existence. [...] A set is not an entity which has an ideal existence. A set exists only when it has been defined. To define a set we prescribe, at least implicitly, what we (the constructing intelligence) must do in order to construct
an element of the set, and what we must do to show that two elements of the set are equal.
Building on the positive integers, weaving a web of ever more sets and more functions, we get the basic structures of mathematics: the rational number system, the real number system, the euclidean spaces, the complex number system, and so forth.
Thus even the most abstract mathematical statement has a computational basis.
The transcendence of mathematics demands that it should not be confined to computations that I can perform, or you can perform, or 100 men ,vorking 100 years ,vith 100 digital computers can perform. Any computation that can be performed by a finite intelligence - any
computation that has a finite number of steps - is permissible.