This paper describes a particular version of constructive
type theory, a subset of the one underlying the Nuprl proof development system,
and it examines its role as a programming environment. Special
attention is given to the property of the theory to talk about
itself. This reflective capability is the basis for automating
proof development and for metalevel programming.