I've seen several times people mentioning that the notion of an algorithm / a computation is taken as a primitive notion in L. E. J. Brouwer's intuitionism. For instance, in *Varieties of Constructive Mathematics* (1987, p.1), Bridges and Richman write that:



> 
> In Bishop's constructive mathematics (BISH), and in Brouwer's intuitionism (INT), the notion of an algorithm, or finite routine, is taken as primitive. Russian constructivism (BUSS), on the other hand, operates within a fixed programming language, and an algorithm is a sequence of symbols in that language.
> 
> 
> 


To the best of my knowledge, Brouwer's intuitionistic mathematics is fundamentally a languageless creation of the mind which is erected on the two acts of intuitionism: (i) the first act gives us the construction that corresponds to the natural numbers; (ii) the second act provides us with the notion of free choice sequents. To put it other way, there is no explicit mention of algorithms.


On the other hand, it seems that this common (?mis?)conception, namely, that the notion of an algorithm is a primitive notion in Brouwer's intuitionisim, came with the influence of the BHK interpretation, where the notion of a proof (which, by the Curry-Horward correspondence, corresponds to the notion of a program) plays the central role in this informal interpretation of intuitionistic logic. However, as I said, this is intuitionistic logic and not Brouwer's intuitionisim - and I do think it helps to keep both apart.


Can we justify this claim that the notion of an algorithm is a primitive notion in Brouwer's intuitionism?



Why is the notion of algorithm a primitive one in Brouwer's intuitionism?
Since the work of Church and Turing (say around 1936), the notion of algorithm is definitely not considered primitive in intuitionism. But Brouwer started intuitionistic mathematics more than 2 decades before (1907, 1912), and in the absence of a commonly accepted notion of algorithm, he formulated his idea (somewhat) like this: 


A sequence of natural numbers arises in the course of time, like a walk through the (infinite) tree $\mathbb{N}^\*$ of finite sequences, choosing at each 'node' a next continuation.


The result is an infinite branch, or an 'arrow' as Brouwer called it. At any node (also right at the start) one may specify a definite finite law which completely governs all next choices (so that there really is no choice left at all). If one does so right at the start, the arrow is called a 'sharp arrow' or a 'lawlike sequence'.


Since the 1930's definition of recursion, it has become standard to identify 'sharp arrow' and 'lawlike sequence' with recursive sequences, I believe. 


