Relationships between the concepts of proof systems and programming languages are known. Some are well demonstrated in systems like Coq and Nuprl, but other aspects have not been fully implemented, such as reflection. I believe that the true context in which such ideas are becoming useful is when they are implemented, this ``implementation as understanding'' principle is the reason some parts of the following text contain code pieces. This should take the form of a logical environment with reflection mechanisms, Nuprl is a good choice since it is used for connecting logic and programming languages. Therefore, the first step towards creating such an implementation should be taken: pinpointing what should be done, and how. This paper is an attempt to do this.