Many specifications and models in proof assistants contain parts that can be translated into executable code. Using generated code instead of re-implementing the model in a target language eliminates a potential source of errors and allows for better integration of formal methods into the software development process. We will present a prototype code generator for the Prototype Verification System (PVS) that will be able to translate a subset of PVS specifications into the Why intermediate language and subsequently to different target languages. The relevance for NASA is illustrated by generating prototype Java code for examples from NASA projects.