SHF: SMALL: Intermediate Languages for Safe and Efficient Compilation

编译器验证的重要性是众所周知的，特别是对于高安全性和高保证的应用程序。无论我们对源代码多么有信心，如果编译器引入了自己的错误和安全缺陷，那么再多的程序验证也无法在编译过程中存活下来。尽管经过验证的编译器在今天已经成为现实，但是今天的编译器编写者所使用的许多技术还没有成为正式的系统。这破坏了对优化编译器正确性证明的信心。这项研究的智力优势在于设计和实现了兼顾安全性和效率的中间语言。工作重点是格拉斯哥Haskell编译器。但是，开发并不局限于特定的语言，而是侧重于更通用的框架。研究的更广泛影响包括改进核实汇编的方法；为编译器的所有阶段提供可靠的语义，使验证更加组合，并使验证更复杂的编译器变得可行。该项目影响的不仅仅是中间语言，因为更广泛的经验教训可以纳入源语言本身。通过正式解决集成依赖类型和效果的困难挑战，这项工作代表了向扩展当前语言的证明能力迈出的重要一步。函数式语言实现在很大程度上依赖于效果来提高效率。例如，Haskell是一种纯函数式语言，但它的实现使用了涉及重赋值的记忆。充分表示实现技术的中间语言必须支持效果。使效果显式不仅增加了对编译器正确性的信心，而且还提供了更多的优化机会来生成更好的代码。当前的研究主要集中在将高级特性向下推入编译管道，这里的目标是将低级特性向上拉入管道。在高级和低级之间找到适当的平衡是具有挑战性的，因为人们希望利用低级特性来提高效率，而不破坏纯粹性的优势，最终阻碍而不是帮助优化。设计有用的中间语言的关键不在于程序必须是纯粹的，而在于它们使用良性效果，即保证功能行为的效果。指导原则是在中间语言的设计和模型中保持与证明理论的紧密联系，特别是那些具有混合调用约定的语言。

The importance of compiler verification is well established, especially for high-security and high-assurance applications. Regardless of how confident we are in our source code, no amount of program verification can survive the compilation process if the compiler introduces its own bugs and security flaws. Even though verified compilers are a reality today, many of the techniques employed by today's compiler writers have not made it into a formal system. This undermines confidence in a correctness proof of an optimizing compiler. The intellectual merit of this research is the design and implementation of intermediate languages that address both safety and efficiency concerns. The work focuses on the Glasgow Haskell compiler. However, the development is not tied to a specific language but focuses on a more general framework. The broader impact of the research consists of improving the approaches to verified compilation; providing a solid semantics for all stages of the compiler makes verification more compositional and makes verifying more complex compilers feasible. The project impacts more than just intermediate languages, because the broader lessons learned can be incorporated into source languages themselves. The work represents an important step toward extending current languages with proving capabilities by formally addressing the difficult challenge of integrating dependent types and effects.Functional language implementations rely heavily on effects for efficiency. Haskell, for example, is a pure functional language but its implementation uses memoization that involves reassignment. Intermediate languages that adequately represent implementation techniques must support effects. Making effects explicit not only increases confidence in compiler correctness, but also presents more opportunities for optimizations to produce better code. Whereas current research has focused on pushing high-level features down the compilation pipeline, the goal here is to also pull low-level features up the pipeline. Finding the right balance between high and low levels is challenging, since one wants to exploit low-level features to enhance efficiency without ruining the advantages of purity and ultimately hindering more than helping optimizations. The key to design useful intermediate languages is not that programs are necessarily pure, but that they use benign effects, namely effects that guarantee functional behavior. The guiding principle is to keep a strong connection with proof theory in the design and models of intermediate languages, especially the ones with mixed calling conventions.