Typer: a Lisp approach to dependent types

为了提高程序的可靠性和程序员的生产率，我们需要使程序员更难引入错误，并尽可能早地捕获这些错误。这意味着我们希望使用高级语言和库，这样程序员可以编写更少的代码，从而减少错误。我们希望使用测试和正式方法来及早捕获错误。 我们使用的方法越轻量级越好，因为程序员的优点之一就是懒惰。到目前为止，最成功的形式化方法是类型检查，例如在Java中就可以看到。 遗憾的是，传统类型只能带给我们这么多。其他技术可以让我们捕获更多的错误，例如模型检查或Hoare风格的逻辑，但代价是要付出更多的工作和专业知识的代价，将这些技术留给利基市场。 我的研究项目提出了一个新的Language Typer，它结合了Lisp风格语言的实用灵活性和在证明助手中使用的强大的依赖类型理论。它的类型系统无缝地涵盖了从传统的简单类型批注到任意复杂的正确性属性的范围。这将使编写和维护其健壮性得到机械验证的软件变得更容易。 当然，Java风格的类型检查的成功并不会立即影响到所有形式的类型检查。要使用额外的功能，您仍然需要额外的工作、额外的注释和额外的专业知识。在某种程度上，这是不可避免的，但仍有很大的改进空间。因此，我的研究计划的重点是让它更容易、更渐进地使用先进类型系统提供的额外动力。 正式的方法已经彻底改变了硬件的设计方式，计算机软件世界也正在经历类似的转变；引领它可以为加拿大的软件行业带来巨大的战略利益。评估这种发展的影响的另一种方法是看看我们整个社会目前对非常简单的计算机病毒的脆弱性。

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.