(By Steve Zdancewic)

As demand grows for trustworthy software infrastructure, large segments of industry are shifting toward newer languages like Java and C#, which offer platforms for large-scale software development, security-critical programming, mobile and embedded code, etc., with strong and well-understood guarantees about portability, memory safety, encapsulation, and other fundamental requirements. These languages are both larger than their predecessors and more ambitious the strength of the safety net they offer to programmers.

A corollary of this trend is that research in programming languages is becoming more concerned with issues of scale and interactions of complex features. At the same time, with language research transitioning into industrial designs much faster than in the past (witness C# and Java generics, which rely on ideas published in conferences only a few years before), the potential costs of errors are magnified.

The safety provided by these languages is enforced by using type systems, which provide a light-weight, programmer friendly way of specifying desirable program properties. To validate strongly typed languages (such as C# and Java), it is necessary to prove that their type systems are sound---that programs accepted by the typechecker comply with the desired safety properties.

Unfortunately, rigorous type-safety proofs even about small programming languages are very difficult for humans to manage: they are long and tedious, with just a few interesting cases sprinkled among many boring ones (which must nevertheless be checked carefully to confirm that they really are boring!). The difficulty of these proofs arises from the management of many details rather than from deep conceptual difficulties (these arise earlier, in the process of getting the definitions right); yet small mistakes or overlooked cases can invalidate large amounts of work. These effects are naturally amplified as languages scale.

A typical example of the current state of affairs can be found in a recent conference paper by Chen and Tarditi (A simple typed intermediate language for object-oriented languages, in POPL 2005) on a new typed intermediate language for compiling object-oriented source languages such as C#. The safety theorem for this language is stated in a standard form (``execution of a well-typed program cannot get the abstract machine into an erroneous state''), and the proof of this fact is regarded by the authors as too boring even to sketch in detail: the paper just says ``By standard induction over the typing rules.'' However, the details of this ``standard'' proof, in the accompanying technical report, run to 26 dense pages! What, realistically, are the odds that anyone besides the authors has checked it carefully? It is a near certainty that a specification of this size contains errors, no matter how many hours of toil have been lavished on paper-and-pencil proofs of correctness. We have quite simply reached the point where purely manual methods of verifying correctness no longer work. (Another point worth noting is that the paper's second author is one of the lead compiler developers at Microsoft: this is not just an academic exercise!)

Automated proof assistants offer the hope of significantly easing these problems. However, despite encouraging progress in this area in recent years, the availability of several mature tools (including Coq, HOL, HOL Light, Isabelle, Lego, NuPRL, PVS, ACL2, and Twelf, and the completion of some astounding tours-de-force in formalizing major theorems of pure mathematics (e.g., Gonthier and Werner's recent formalization of the four-colorability theorem), the application of these tools to programming language problems is not commonplace.

This section outlines some challenges to be addressed with respect to formal verification of programming language metatheoretic properties (such as type safety) using theorem provers and other proof assistant technology.

Challenges:

• Developing appropriate theorem proving infrastructure for dealing with alpha-conversion and manipulating language syntax with variable binding structure. Several techniques, such as de Bruijn indices, higher-order abstract syntax, and nominal logic, have been proposed, but they have been mostly applied in specific settings. More general support for structures-with-binding is critical.
• Developing a library of modular components, such as type environments, finite sets, etc, that can be reused in different language formalization contexts. Such a library might consist of a collection of domain-specific data structures for manipulating programming language syntax, specifying inference rules, and defining semantics, along with appropriate collections of lemmas and tactics for manipulating those data structures.
• Demonstrating the applicability of the tools and techniques developed to address the first two challenges for problems relevant to programming language type systems. Here, issues of scale and expressiveness can be tested: how well do the mechanized proofs scale to real programming language concepts and how well can they be used for standard proof techniques such as logical relations and bisimulations.