We, of course, cannot predict all the problems that will arise, nor all the innovations that will result, but we can guarantee that we will generate a useful body of reference material, introductory lessons grounded in this material, collections of these lessons, and a proven mechanism for collecting feedback from readers of the material. Web access to this material will inform, if not transform, the teaching of various topics in college mathematics and computer science.
The research we are doing now combining Nuprl with a symbolic algebra system and our work in support of numerical computation have the potential to greatly broaden the scope and impact of our plans over the course of the next several years. So there is a chance that we can do even more than is scheduled here. The methodology proposed also has the potential to deepen our understanding of pedagogy. Our experience is that tactics are an effective way to teach technique. We can measure students progress as they learn to master the basic tactics. These combined with the basic tacticals (THEN, ORELSE, REPEAT) allow students to express methods of solving problems and will encourage them to reflect on skill acquisition.
As we make connections between more and more subjects, from logic to circuits and algebra, students will see that one major component of understanding is linking new knowledge tightly into a solid base of fundamental concepts.