This is a short report from my workshop on programming with dependent types, which took place at the Heidelberg Laureate Forum, September 23, 2013. There were 18 participants in the workshop, including four ACM Turing award laureates: Vinton Cerf, Butler Lampson, Dana Scott, and Robert Tarjan. At the beginning of the workshop, I presented some background on dependent types and argued that they are useful in programming, in addition to their well-known usefulness in proof assistants for constructive mathematics.

The first point of discussion was sigma types, which I suggested are very useful for validity propagation in normal computer programs. For example, a system requiring a Unicode string would validate the input once and pass on an element of a sigma type consisting of the original string together with a proof that it satisfies the Unicode predicate. This claim was challenged by Lampson who argued that the same could be achieved by inheritance. Later in the talk I said that this isn’t completely true as predicates can be combined arbitrarily in ways that subclasses cannot. For example, it is trivial to define the type of strings of uppercase Unicode strings of length at most 100 using a sigma type, but an inheritance hierarchy supporting these types would have to be very complicated.

Next, I mentioned that general recursion has to be given up in type theory: Lampson found this a severe limitation. I argued that general recursion seldom is used in systems programming. There were some different views on this among the audience, and Lampson suggested that it would be an interesting topic for an empirical study. One of the participants made the very interesting remark that successful programming languages have one thing that they are really good at – a killer feature, as it were. We discussed possible killer features for a dependently typed programming language.

After the presentation, we spent some time talking about software verification in general. Lampson made a distinction between approximate software, such as a search engines, and precise software, such as banking software. One participant asked about the relation between programming with dependent types and model checking. Vint Cert, among others, suggested that they are complementary, giving memory allocation in a multicore environment as an example where model checking could be useful even if the individual functions of the system were verified independently. We discussed testing versus formal verification and the reasons why verification seldom is used in industry. Vint Cerf made the general remark that one of the main obstacles to the adoption of verification features in programming languages is that programmers are lazy.

Lampson spoke about an experience he had with dependent types for a module system, which project was eventually abandoned, as his module types in most cases could be replaced with link time validation, which is much easier. He also mentioned that the way forward for dependent type theory was to implement it and give empirical evidence for its usefulness. He also raised some skepticism about the feasibility of this project. Vint Cerf argued that incremental changes to existing programming languages could have much larger impact than a completely new programming language based on dependent types.

We also talked about the difference between proof assistants and programming languages: one participant mentioned that algorithms extracted from proof often are suboptimal. Next, we talked about the kind of error messages that would be produced by a dependently typed programming language and how useful they would be for locating the source of the errors. I made a case for not using higher order unification or the Hindley-Milner type inference algorithm, as these approaches often give rise to incomprehensible error messages.