Typer: a Lisp approach to dependent types

为了提高程序的可靠性和程序员的生产力，我们需要让程序员更难引入bug，并尽可能早地捕获这些bug。这意味着我们希望使用高级语言和库，这可以让程序员编写更少的代码，从而减少错误。我们希望使用测试和形式化的方法来尽早发现bug，我们使用的方法越轻量级越好，因为程序员的优点之一就是懒惰。目前为止，最成功的形式化方法是类型检查，例如在Java中。遗憾的是，传统类型只能让我们走到这一步。其他技术让我们捕捉更多的错误，例如模型检查或霍尔风格的逻辑，但在成本上更多的工作和专业知识，离开这些技术niches.My研究计划提出了一个新的语言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.