More than just a user's manual for a specific system, this book serves as an introduction to a very expressive foundational theory for mathematics and computer science, a theory which brings together many diverse ideas in modern computing theory. The book is also an introduction to formal logic in general and to constructive logic in particular, and it introduces new methods of program development and verification.
This book also describes a computer system for doing mathematics. The system provides a medium distinct from the traditional paper and blackboard, an active medium that can detect errors, implement tedious steps of argument or computation and carry out suggestions for building proofs. In a new level of precision is made useful.
This book also introduces an ongoing enterprise and a new area of research. It presents a first example of the kind of system that we believe will become significant in the next decade. There is clearly much to be done in this area, and this document will make readers aware of certain open problems and challenging tasks.