As a programming language
is similar to functional programming languages with a rich type structure such as Edinburgh ML. However, the type structure of is richer than that of any existing programming language in that it allows dependent functions and products as well as sets , quotients and universes. Moreover, our approach to type checking enables the user to design automatic type--checking algorithms which extend those of other type systems. There are interesting connections between concepts in and various new ideas being suggested for programming languages; see for example Russell [Donahue & Demers 79] , Pebble [Burstall & Lampson 84] and Standard ML [Milner 85].
Presently is only interpreted, so it is much slower than languages with compilers. However, for a simpler subsystem, , an optimizing compiler has been implemented (see [Sasaki 85]). There are many challenging issues here for people interested in building a new kind of optimizing compiler, as, for instance, the fact that programs usually occur in the context of their specifications means that there is more information available for good optimizations than is typically the case.
is also a formal logical theory, so one would expect a connection with logic programming and with PROLOG [Clocksin & Mellish 81]. In fact it is possible to express some aspects of PROLOG in a subset of and to use a linear resolution tactic to execute specifications in this subset. does not optimize such a proof tactic, however, so the execution would be slower than in existing PROLOG evaluators. Moreover, the usual way to use theorem--proving power computationally in involves proving a theorem of the form for all x of type A there is a y of type B such that
and then extracting a program from this proof. Thus in a theorem prover is used more as a compiler than as an evaluator.