SHF:Small: Bringing Extensibility and Performance to Verified Compilers

编译器是软件开发的核心工具。 它的作用是将程序员编写的人类可读代码转换为计算机可以理解的机器代码。 由于编译器创建了在计算机上运行的实际机器代码，因此错误的编译器可能导致灾难性的故障，包括医疗设备，电传飞行航空软件和汽车系统中的错误。 这项研究将导致更可靠的编译器，最终将增加我们对现在在我们日常生活中无处不在和安全至关重要的软件的信心。该项目将开发用于构建编译器的新技术，以确保最高水平的严格性和可靠性，以便我们可以肯定地知道，在计算机上运行的机器代码完全按照程序员的意图运行。 为了实现这一目标，主要研究者将研究如何使用证明助手来实现正式验证的编译器。 更具体地说，该研究将探索使Compcert等经过正式验证的编译器生成更好代码的技术，以便它们与GCC和LLVM等主流编译器更具竞争力。 此外，本研究还将探讨减少证明负担的方法，以便可以更容易地开发和更新像Compcert这样经过验证的编译器。 最终，本研究将使形式验证编译器成为主流，从而使其更广泛地被程序员使用。

The compiler is a tool that is central to the development of software. Its role is to translate the human-readable code written by a programmer into machine code that a computer can understand. Because the compiler creates the actual machine code that runs on the computer, a faulty compiler can lead to catastrophic failures, including errors in medical devices, in fly-by-wire aviation software, and in automotive systems. This research will lead to more reliable compilers, which in the end will increase our confidence in the software that has now become ubiquitous and safety-critical in our daily lives.This project will develop new techniques for building compilers to ensure the utmost level of rigor and reliability, so that we can know with certainty that the machine code running on the computer does exactly what the programmer intended it to do. To achieve this goal, the principal investigator will investigate ways of using proof assistants to implement formally verified compilers. More specifically, the research will explore techniques for making formally verified compilers like Compcert generate better code, so that they can be more competitive with mainstream compilers like GCC and LLVM. Furthermore, the research will also investigate ways of decreasing the proof burden, so that verified compilers like Compcert can be developed and updated more easily. In the end, this research will enable formally verified compilers to become more mainstream, so that they can used more broadly by programmers.