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.