What does it mean for a programming language to exist? Languages are usually defined by an informal description augmented by a reference compiler whose behavior is regarded as normative. This approach works well so long as a single reference compiler suffices, but as soon as there are multiple implementations, it is necessary agree on what language they implement. This is typically achieved through social processes such as standardization committees that build consensus and impose norms.

These processes have served us well, and will continue to be important for language design. But they are not sufficient to support the level of rigor required to prove theorems about languages and programs written in them. For that we need a semantics, which provides an objective foundation for such analyses. But merely having such a rigorous definition for a language is not enough @y(M) it must be validated by a body of meta-theory that establishes its coherence and its consistency with expectations.

But how are we to develop and maintain this body of theory? For full-scale languages the task is so onerous as to inhibit innovation and foster stagnation. The way forward is to take advantage of the recent advances in mechanized reasoning. By representing a language definition within a logical framework we may subject it to formal analysis, much as we use types to express and enforce crucial invariants in our programs. I will describe the use of the Twelf implementation of the LF logical framework, and discuss the successes and difficulties in using it as a tool for mechanizing the meta-theory of programming languages.