Compilers that Preserve and Enforce Invariants and Proofs

本程序的目标是通过设计新的软件开发工具来保证用于实现所有程序的机器码，从而使软件更加可靠。我们依靠软件来控制从航天器到心脏起搏器的一切。这意味着即使是简单的软件错误，比如把英制单位的数字误认为公制单位，也会造成数百万美元的损失和生命损失。高保证软件领域寻求防止软件错误，但是这个过程是昂贵和耗时的。该研究计划将通过创建自动排除机器代码中所有类型错误的新工具来简化高保证软件开发。

The goal of this program is to make software more reliable by designing new software development tools that provide guarantees about the machine code used to implement all programs. We rely on software to control everything from spacecraft to pacemakers. This means even simple software errors, such as mistaking a number in imperial units for a number in metric, cause millions of dollars in damages and cost lives. The field of high-assurance software seeks to prevent software errors, but the process is costly and time consuming. This research program will simplify high-assurance software development by creating new tools that automatically rule out whole classes of errors in machine code. Machine code is usually generated from programming languages that simplify software development by hiding the details of how computers execute 0s and 1s. For example, we think about numbers in decimal, the digit 0--9, while computers represent numbers as sequences of 0 and 1 such as "101" (the number "5"). A compiler is a program generates machine code, e.g., translates "5" into "101". Languages often provide tools for reasoning about invariants---properties of a program that must always be true for the program to be correct. For example, some languages can prevent a program from using the imperial unit "5 ft" when a metric unit "5 m" is expected (which would have prevented the Mars Climate Orbiter disaster and saved $300 million). In these languages, the compiler checks that the invariant holds before trying to generate machine code. A few languages, such as so-called dependently typed languages, allow the programmer to encode program invariants and proofs of correctness. Writing invariants and proofs requires extra work at first, but allows the programmer to prove that their program is safe, secure, and correct. This is necessary since, in general, we cannot automatically check arbitrary invariants, but we can check programmer provided proofs. Unfortunately, compilers for dependently typed languages do not preserve all the invariants programmers can express. So for example, while "5 ft" and "5 m" are different, the compiler will translate both to "101", allowing errors like "5 ft + 5 m = 10" even in a "proven correct" program. This research program will design and develop new compilers that translate dependently typed programs into machine code while preserving invariants and proofs. By making compilers preserve more of what a programmer is thinking, we improve the reliability of all programs. In the short-term, this research can reduce the cost of high-assurance software, such as the software running in cars and medical devices, by providing tools to automatically rule out classes of errors. In the long-term, this work can reduce the cost and improve the performance of a broad range of software, from games to scientific computations, by allowing developers to better communicate with the compiler as it generates efficient machine code.