CAREER: Verified Compilers for a Multi-Language World

职业：多语言世界的验证编译器编译器在软件生产中起着至关重要的作用。因此，他们应该是正确的。也就是说，它们应该保留它们编译的所有程序的行为。尽管近年来在经过正式验证的编译器方面取得了显著进展，但这些编译器存在一个严重的局限性：它们被证明是正确的，前提是它们只会被用来编译整个程序。这是一个完全不切实际的假设，因为今天的大多数软件系统都是由用不同语言编写的组件组成的，这些组件由不同的编译器编译成一个通用的低级目标语言。这个项目的智力价值在于开发了一个证明架构，用于为当今的多语言软件世界构建经过验证的编译器：这种经过验证的编译器保证了组件的正确编译，并支持与任意目标代码的链接，无论其来源如何。该项目更广泛的意义和重要性在于，组件的验证编译实际上对每个软件系统都有好处，从安全关键软件到web浏览器，因为这些系统使用用各种语言编写的库或组件。该项目将通过以下开发实现广泛的影响：(i)可扩展到现实的多通道编译器和多语言软件的证明方法，（ii）扩展LLVM的目标语言-越来越多的现代编译器选择的目标语言-支持从类型安全的源语言进行编译，以及（iii）与本项目过程中使用的证明技术相关的教育材料。该项目有两个中心主题，这两个主题都源于编译器正确性作为语言互操作性问题的观点。首先，组件编译正确性的规范需要源语言和目标语言之间互操作性的形式化语义。更准确地说：如果源组件（比如s）编译为目标组件（比如t），那么t与任意目标代码（比如t‘）链接的行为应该与s与t’互操作的行为相同。其次，要实现从Java、Rust、Python和C等不同语言编译的组件之间的安全互操作性，需要设计一种基于LLVM的逐渐类型安全的目标语言，该语言支持更精确类型、更不精确类型和类型不安全组件之间的安全互操作性。

Title: CAREER: Verified Compilers for a Multi-Language WorldCompilers play a critical role in the production of software. As such, they should be correct. That is, they should preserve the behavior of all programs they compile. Despite remarkable progress on formally verified compilers in recent years, these compilers suffer from a serious limitation: they are proved correct under the assumption that they will only be used to compile whole programs. This is an entirely unrealistic assumption since most software systems today are comprised of components written in different languages compiled by different compilers to a common low-level target language. The intellectual merit of this project is the development of a proof architecture for building verified compilers for today's world of multi-language software: such verified compilers guarantee correct compilation of components and support linking with arbitrary target code, no matter its source. The project's broader significance and importance are that verified compilation of components stands to benefit practically every software system, from safety-critical software to web browsers, because such systems use libraries or components that are written in a variety of languages. The project will achieve broad impact through the development of (i) a proof methodology that scales to realistic multi-pass compilers and multi-language sofware, (ii) a target language that extends LLVM---increasingly the target of choice for modern compilers---with support for compilation from type-safe source languages, and (iii) educational materials related to the proof techniques employed in the course of this project.The project has two central themes, both of which stem from a view of compiler correctness as a language interoperability problem. First, specification of correctness of component compilation demands a formal semantics of interoperability between the source and target languages. More precisely: if a source component (say s) compiles to target component (say t), then t linked with some arbitrary target code (say t') should behave the same as s interoperating with t'. Second, enabling safe interoperability between components compiled from languages as different as Java, Rust, Python, and C, requires the design of a gradually type-safe target language based on LLVM that supports safe interoperability between more precisely typed, less precisely typed, and type-unsafe components.