Recently two formerly unknown articles by Errett Bishop (1928-1983) were posted online by Martín Escardó. One is entitled "A general language", deals with constructive type theory, and is 28 pages long. The other is entitled "How to compile mathematics into Algol", deals with implementation of his constructive type theory, and is 29 pages long. Both pdfs can be found here.
Numerous intriguing questions arise in connection with these articles, such as the following:
Question 1. What is the precise date of composition of the articles?
Question 2. Why weren't the articles published?
Question 3. What led Bishop to develop a constructive type theory, given what is often considered to be his lack of interest in formal logic and formalisation of constructive mathematics? (see Note 1 below).
Question 4. Should our perceived views of Bishop's foundational stance be reconsidered in light of these manuscripts?
Question 5. Since the manuscript "A general language" and Bishop's 1970 published article "Mathematics as a numerical language" are very different, could somebody summarize the similarities and differences between the two?
Note 1. For example, one finds the following comment by a selfdeclared constructivist:
the constructive mathematician dismisses classical mathematics as an exercise in formal logic (see Richman, Fred. Interview with a constructive mathematician. Modern Logic 6 (1996), no. 3, 247-271).
This is not an indication of great esteem for formal logic on the part of this particular constructivist.
Note 2. It must be said that Bishop himself was not averse to making statements of this sort:
It is not surprising that some of Brouwer's precepts were then formalized, giving rise to so-called intuitionistic number theory, and that the formal system so obtained turned out not to be of any constructive value. In fairness to Brouwer it should be said that he did not associate himself with these efforts to formalize reality; it is the fault of the logicians that many mathematicians who think they know something of the constructive point of view have in mind a dinky formal system or, just as bad, confuse constructivism with recursive function theory. (page 4 in "A constructivist manifesto", chapter 1 in Bishop, Errett. Foundations of constructive analysis. McGraw-Hill Book Co., New York-Toronto, Ont.-London 1967)