One point made here is that formal constructive mathematics can be interpreted as a "high-level" programming language; another point is that there are good reasons for doing so. Among them is the fact that a theoretical basis for automatic program writers (APW's) becomes especially perspicuous (in such a context the problem of assigning meaning to programs a la Floyd [6] is the inverse of program writing). Another reason is that such an interpretation reveals a number off interesting mathematical problems in the theory of computing. While making these points we find occasion to present new observations on the completeness and efficiency of automatic program writers and to formulate a specific example of what we call von Neumann's principle on the logical complexity of systems. We apply the principle in the automatic program writing context and discuss its more general ramifications about the intelligibility of programs.