Lambda the Ultimate

...is indeed to ensure correctness (no scare quotes because I'm interested in using a theorem prover satisfying the de Bruijn criterion written in a language with a formal semantics and built with a certified compiler running on a processor almost certainly specified and verified using Z or something very similar). Correctness of what? Correctness of treatment of properties that are extraordinarily difficult to get right without such tools. My argument is that the next mainstream programming language needs to get two things really right that, today, no language manages at the same time:

• Concurrency
• Information flow security

Both of these have proven highly resistant to informal treatment. The state of the art for dealing with concurrency outside of process algebras seems to be message-passing, and that imposes limitations on the runtime architecture and programming model, along the lines of Erlang or E, for example. If you can live with that, great, but many systems can't, which is why people are interested in process calculi, software transactional memory, and so on.

Security is a huge topic, and interesting because it has both static and dynamic components. E is the gold standard here, but has essentially no static component. I'd like to see something like Flow Caml but with the necessary dynamic component included. This is a horribly inadequate description of the goal; a much better description, along with details about one effort to address it, can be found in Geoffrey Washburn's Principia Narcissus.

So if you think in terms of a JoCaml + Flow Caml + some stuff that neither of them do, like addressing the dynamic aspects of information flow control, you'll see that there's some rather heavy type-theoretic lifting to do. It's brutally hard to get that stuff right when you are being formal, let alone when you aren't. In addition, if you want people to use your language, you have to not violate their existing mental models too much, either in terms of apparent semantics or in terms of syntax. This is where I draw most of my inspiration from Tim Sweeney's work. Tim is putting a great deal of effort into making the language that he is working on look like another object-oriented/imperative/functional hybrid whose syntax resembles a cross between ML's and Pascal's, but whose semantics might resemble something like a dependently-typed Disciple more than anything else.

I think that's what the next mainstream language is going to have to be like, if it's to be anything besides another warmed-over C/C++/Java/C# or Lisp/Smalltalk/Python/Ruby clone. Neither multiprocessor/multicore systems nor the Internet are going away; the days of writing Von Neumann code that only has to deal with one implicitly-trusted user are long behind us. But addressing those issues is hard, and it will take the absolute best practices we can bring to bear on designing and implementing programming languages to tackle them effectively.

So that leaves scaling this stuff up to real languages. That's the big outstanding challenge, and is part of why I'm excited about the potential of Adam Chlipala's work with LambdaTamer. I think his program of using denotational semantics so that the metalogic is Coq's own Calculus of Inductive Constructions and "proofs" of semantic equivalence are just CIC equality, coupled with aggressive generic proof automation, is the path to scaling efforts like this up. Of course, this remains hypothetical; there's a great deal more work to be done to confirm this hypothesis. But it seems to me to be the most promising path.

I don't know how closely this set of thoughts tracks those of anyone else who is interested in certified software development. But I do think it helps explain why you can come away from Winskel and the Semantics Survey in Coq that's based on it not really feeling like it's worth it for the little IMP language that Winskel develops, but perhaps you can see how it could be worth it for a kind of combined JoCaml/Flow Caml/Disciple that won't scare people away. :-)

Studying programming languages without formal semantics would be like studying physics without math. It would make the study of programming languages an exclusively soft science. Formal semantics help us understand programming languages, give us confidence in the truths we discover about languages, and prevent us from believing things that aren't true. They provide tools for exploring new semantics rigorously — many (most?) of the advances in programming language theory have arisen out of formal semantics.

If formal semantics has any applications other than that, that's just a bonus. But there are some: for example, they're very useful in the design of languages. The security examples given by Paul are just one example of this. Formal semantics provide general patterns for language design, which can be applied to new languages.