New articles by Errett Bishop on constructive type theory?

Question

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)

Answer 1

Re (1): in this presentation by Iosif Petrakis the manuscripts are dated 1969(?). There is a 1970 published article from a 1968 conference with a similar topic as the unpublished "Compiling Mathematics into Algol". Erik Palmgren (arXiv:1201.6272) refers to this latter work as "Unpublished text for a seminar – 1970."

Re (2): from this comment by Bas Spitters I understand that it was Bishop's decision not to publish these manuscripts.

Re (3): Petrakis explains that it was Bishops intention to implement his framework for constructive mathematics into some computer language. For that purpose it was unavoidable that he could describe the algorithms with enough precision to be intelligible to machines, hence his interest in the formalisation of constructive mathematics. _{A quote from Bishop's Algol paper: "Formal constructive mathematics is concerned with the communication of algorithms with enough precision to be intelligible to machines".}

Answer 2

Regarding Question (2), I have heard the following story from (non-constructivist) people who knew E. Bishop well:

Bishop had submitted (some of) these papers for publication, but they were not accepted in their then form. The reasons (as pointed out by either the editor or referees) was that other people had been working on similar topics with better/similar results. Bishop then set about improving his own papers/results, trying to formulate (what we now call) explicit type constructors everywhere. Unfortunately, Bishop died before he could finish this endeavour.