The Nuprl system has six major components: a window manager, a text editor, a proof editor, a library module, a command module and a function evaluator. Interaction with Nuprl takes place in the context of three languages---the command language, which is extremely simple, the object language, which is the mathematical language of the system, and the metalanguage, which is a programming language with data types referring to the object language. The command language is used to initiate editing, use the library and initiate executions in the object and metalanguages, to name a few of its functions. The object language is a constructive theory of types. The metalanguage is the programming language ML from the Edinburgh LCF system modified to suit Nuprl .
The window manager provides the interface for the interactive creation of certain kinds of linguistic objects called definitions, theorems, proofs and libraries on a terminal screen. Windows offer views of objects; using these views the user can navigate through the object, stopping to modify it, to copy parts of it to other windows or to insert parts into it from other windows, etc. Three special windows provide for editing theorems, viewing the library and entering commands.