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.