In a Logical Programming Environment, we can reason directly about running code. Nuprl uses a dialect of ML as its programming language, and it has another mechanism for linking specifications to code that the Cornell group pioneered, namely, programs can be synthesized from constructive proofs that a programming task is solvable. The rules for the logic guarantee that the extracted code meets the specifications.