A Universal Core Language

One of my long-term research goals (and likely, a significant portion of my dissertation) is the design of a very powerful, very general core language and type system. To be clear, a core language is a reduced set of syntactic forms generally not meant for human consumption. The purpose of the core language is to define the semantics of the language, and to be able to prove theorems about it. A compiler will translate a program into the core language, which it will then type check and subsequently translate into IR.

One idea I do want to explore is widening the gap between concrete syntax and core. The overall idea is that concrete syntax should be designed to be "nice" for people to use, perhaps even designed by legitimate designers. However, this is a topic for another post.

The core I envision could operate as a substrate for many programming languages, and would bring a very powerful dependent type system to bear for the purposes of verification. My philosophy with regard to dependent types is that they should be a tool, but not a hindrance. A dependently-typed language should separate the decidable and undecidable portions of its typechecking, allowing proof obligations to be ignored or deferred. However, a language which generates these kinds of obligations makes verification, testing, and many other tasks significantly easier.

I want to try to combine several things that don't tend to play nicely together: 1) impredicative polymorphism, 2) subtyping, 3) full higher-order dependent types, and 4) types describing concurrent behaviors. The final goal is made possible by my own work, and integrates well with the third. The first two lead to undecidability when combined, which is usually bad, but I don't particularly care, since the pathway to the last two begins with the sign "Abandon all decidability, ye who enter here".

The real difficulty lies in designing a logic which combines the first two and the last two, and is sound. Decidability can be sacrificed; soundness cannot. And one of the first things you learn as a logician or an algebraist is that there are fundamental limitations upon what kinds of reasoning systems one can design.

But assuming I can do this, the resulting core language would be quite powerful. For one, it would be possible to verify concurrent programs with arbitrary primitives. It would be possible to embed a language with a weaker type system (say, predicative or ad-hoc polymorphism) by synthesizing the necessary subtyping proofs by using the (decidable) type checking algorithms for those type systems. A similar approach could be used with substructural types, region types, and other interesting decidable type systems. In other words, it could act as a substrate for other languages- in essence, a universal core language.

If nothing else, this would provide a convenient mechanism for getting test examples. If I can embed languages like ML, Haskell (or Java, Scala, X10, or whatever...) in this core, then I can simply translate existing programs. Of course, none of them will have any proofs of correctness for the obligations they generate, but this could be a positive, as it gives me an opportunity to show the utility of the type system I want to design.