A revisionist computer science interpretation of his "Dialectica theorem" explains how his "proofs" were high-level specifications of functions, with formal demonstrations that the functions terminated on suitable inputs; his "constructive content" consisted of computer programs to implement the functions, where the programs are guaranteed to terminate. In essence, Kurt Godel invented a method for program synthesis from specifications.

In explaining this cleaned-up version of Godel's theorem, due to Jean-Yves Girard and further clarified by Daniel Leivant, we learn how a logician programs with inductively defined data. This case study explains the core ideas of the so-called "Curry-Howard correspondence"--- how data types are really theorems, and how typed programs are really proofs.

The software engineering methodology we explain also gives a version of Godel's incompleteness theorem for computer science: all programs synthesized from formal proofs can be proven to terminate, but a proof of that general truth cannot be represented in the logical system. A direct consequence of this theorem is of particular interest to computer scientists: in the language used to code programs that are synthesized from specifications, we cannot implement a (metacircular) interpreter.