Typer: a Lisp approach to dependent types

点击翻译按钮获取中文摘要

To improve program reliability and programmer productivity, we need to make it harder for the programmer to introduce bugs, and to catch those bugs as early as possible. That implies we want to use high-level languages and libraries, which let the programmer write less code and hence fewer bugs. And we want to use testing and formal methods to catch bugs early. The more lightweight the method we use, the better, since one of the virtues of programmers is laziness. The most successful formal method around is by far type checking, as seen for example in Java. Sadly, traditional types only bring us so far. Other techniques let us catch more bugs, e.g. model checking or Hoare-style logic, but at the cost of a lot more work and expertise, leaving those techniques to niches. My research program proposes a new language Typer, which combines the pragmatic flexibility of Lisp style languages with the powerful theory of dependent types used in proof assistants. Its type system seamlessly covers the range from traditional simple type annotations to arbitrarily more complex correctness properties. This will make it easier to write and maintain software whose robustness is mechanically verified. Of course, the success of Java-style type checking does not immediately carry over to all forms of type checking. To make use of the extra power, you still need extra work, extra annotations, and extra expertise. To some extent this is unavoidable, but there is still a lot of room for improvement. So the focus of my research program is on making it easier and more incremental to use the extra power provided by advanced type systems. Formal methods have revolutionized the way hardware is designed, and the world of computer software is going through a similar transformation; leading it can bring large strategic benefits to the software industry in Canada. Another way to evaluate the impact of such a development is to look at the current vulnerability of our society as a whole to very simple computer viruses.