Criticisms

Of course, as with almost any significant enterprise, one can criticize various aspects of this proposal. Indeed, here are some criticisms one might expect along with a reply.

1. Some people who have never seen a system with a definition and display facility or who have only seen Lisp-like syntax for formal mathematics might complain that formalism is too difficult to read. But the examples presented here and in the appendix are taken directly from the system, and one can see for oneself how readable they are.

2. Since computer systems can be intrusive and consume a lot of time in programming courses, one might complain that the computer will get in the way of content. But the primary use of the software is for reading in the style of Netscape which are extremely convenient and can be explained to an elementary school student in minutes. This level of computer skill, ``point-and-click,'' is a basic as reading. Furthermore, any advanced features of Nuprl which we find useful can also be presented in this style.

3. The formal aspect of the mathematics is one more concept to learn. It can be argued that the added value is not worth the cost. But the highest cost is for the producer of the material. We have already incurred much of that cost in our research since the mathematics is already formalized. We have shown that several problems are solved by the formalism (in 3.1). The project will attempt to assess the costs and benefits more carefully, especially the value of teaching logic as part of the formalization process rather than as an isolated topic.

4. There is some added cost to formalism, so someone might claim that the cost will make the material inaccessible to average students. There is no evidence to support this claim. Indeed, David Gries, a distinguished educator and co-author of the book A Logical Approach to Discrete Mathematics [36] has collected evidence to the contrary, showing that the average students benefit from the clarity and definiteness of a formal calculus. My own experience is similar as is experience with the more ambitious computerized tutors [3], and in a course teaching logic, some formalism must be taught.

5. The methods being investigated are only useful in mathematical courses with a rigorous foundation, and someone might claim that this is a limited part of the curriculum with little impact below the second year in college. Of course, a great deal of mathematics is based on rigorous foundations. We can imagine these methods being helpful in algebra, geometry and calculus and eventually in physics, mechanical engineering, etc. Already there is a significant effort to deploy similar tools for geometry instruction in high school [5][3]. These techniques have value both above and below the first and second year of college.

6. Finally, someone who is unwilling to support an experiment without knowing the outcome might say The Cornell group does not have enough classroom experience with the tools to guarantee success at the right level. But we are seeking the funds to acquire more experience and present the results of our work. We have offered the material in advanced courses with our own resources gaining a great deal of experience which informs this proposal. This led to the ideas presented here, a plan with modest aims and a large chance to succeed. The experience also led to changes in the system to make it more accessible. So we have already done the ground work.

In summary, we see that these criticisms are unwarranted for this project. The essential point is that we are promising to produce an exciting new product of wide value which will capitalize on a large NSF research investment to create added investment in education. We have a proven record of delivering excellent research, and we will deliver in education as well.