Compilers that Preserve and Enforce Invariants and Proofs

本程序的目标是通过设计新的软件开发工具来保证用于实现所有程序的机器码，从而使软件更加可靠。我们依靠软件来控制从航天器到心脏起搏器的一切。这意味着即使是简单的软件错误，比如把英制单位的数字误认为公制单位，也会造成数百万美元的损失和生命损失。高保证软件领域寻求防止软件错误，但是这个过程是昂贵和耗时的。该研究计划将通过创建自动排除机器代码中所有类型错误的新工具来简化高保证软件开发。机器码通常由编程语言生成，通过隐藏计算机如何执行0和1的细节来简化软件开发。例如，我们考虑十进制数字0- 9，而计算机将数字表示为0和1的序列，例如“101”（数字“5”）。编译器是生成机器码的程序，例如，将“5”翻译成“101”。语言通常提供了推理不变量的工具，不变量是指程序必须始终为真才能使程序正确的程序属性。例如，某些语言可以阻止程序在使用公制单位“5米”时使用英制单位“5英尺”（这将防止火星气候轨道器的灾难并节省3亿美元）。在这些语言中，编译器在尝试生成机器码之前检查不变量是否成立。一些语言，比如所谓的依赖类型语言，允许程序员对程序不变量和正确性证明进行编码。编写不变量和证明一开始需要额外的工作，但允许程序员证明他们的程序是安全的、可靠的和正确的。这是必要的，因为一般来说，我们不能自动检查任意不变量，但我们可以检查程序员提供的证明。不幸的是，依赖类型语言的编译器不能保留程序员可以表达的所有不变量。例如，虽然“5英尺”和“5米”是不同的，但编译器会将两者翻译为“101”，即使在“证明正确”的程序中也会出现“5英尺+ 5米= 10”这样的错误。该研究计划将设计和开发新的编译器，将独立类型的程序转换为机器代码，同时保留不变量和证明。通过让编译器更多地保留程序员的想法，我们提高了所有程序的可靠性。在短期内，这项研究可以通过提供自动排除各类错误的工具，降低高保证软件的成本，例如在汽车和医疗设备中运行的软件。从长远来看，这项工作可以降低成本，提高从游戏到科学计算的各种软件的性能，因为它允许开发人员在编译器生成高效的机器码时更好地与编译器通信。

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.