We mention philosophy because in a sense Nuprl embodies a philosophy of mathematics. It demonstrates that it is possible to conduct a "mathematical discourse" with a computer. We can trace backwards from the interactions to the principles of physics and information science that determine the outcome of that interaction. So, we can reduce explanations of mathematical discourse to basic principles. This is a contribution to an analysis of the foundations of mathematics, which is a philosophical matter.
We also notice that the potential for more elaborate and extensive mathematical discourse with Nuprl is apparently unlimited. As we push forward into the more complex realms of this interaction, we will see what else can be reduced to these same primitives. This enterprise means that we will always be engaged in a philosophical as well as a scientific investigation.
A simplistic view of the philosophy of mathematics says that there are four schools of thought: Platonism; Logicism; Formalism; and Intuitionism. Actually there are many variations and distinctions, but we will not elaborate beyond a simple model for now. These schools can be summarized as follows.
Our work shows that we can communicate mathematics to computers endowed with a certain physical structure, say electronic digital computers that can implement universal computers in the sense of Turing and Church. It suggests that meaning can arise out of mental capabilities. In this sense the ideas of Kant, Brouwer and Chomsky seem to shed light on the enterprise. The Platonic notion is perhaps not so useful. Formalism does not seem to recognize the fact that certain computational abilities are necessary and are essential parts of the formal language and hence essential parts of an explanation of what enables mathematical discourse. As for Logicism, this might just be a matter of definition. In the case of Nuprl's contructors, we might say that if we remove that natural numbers as primitive but keep recursive type definitions, then we can rebuild the numbers and hence the rest of mathematics. But we need the "higher order" parts of logic, namely functions.