next up previous contents index
Next: The ``Feel'' of Up: Overview Previous: Programming Modes

Physical Characteristics

The system described here is written in about 60,000 lines of Lisp. It runs in Zetalisp  on Symbolics  Lisp Machines and in Franz Lisp  under Unix 4.2BSD.  There are also several thousand lines of ML programs included in the basic system. We have been using it since June 1984 principally to test the ideas behind its design but also to begin accumulating a small library of formal algorithmic mathematics. It can be used as a programming  environment, and to a limited extent it has seen such service. But unlike its simpler predecessor, [ Staff 83] , it has not been provided with a compiler  nor an optimizer, so it can be very inefficient. We hope that in due course there will be facilities to make it run acceptably fast. The system is in fact growing, but the major thrust over the next year is to substantially enhance its deductive power and its user--generated knowledge in the form of libraries of definitions, theorems and proof methods (see section 1.9 for some of our detailed plans).

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995