SHF: Small: Principled Compiling and Linking for Multi-Language Software

在构建大型软件系统时，程序员应该能够为系统的每个部分使用最好的语言。但是，当用一种语言编写的组件成为多语言系统的一部分时，它可能会与具有原始语言中不存在的功能的组件进行互操作。这会影响程序员在重构代码时(即，做出应该导致相同行为的更改)。由于程序在编译后与公共目标进行交互，因此程序员在进行正确重构源代码组件的推理时，必须了解链接和目标级交互的细节。不幸的是，当组件在多语言系统中使用时，目前还没有可用的软件工具链来支持单语言推理。该项目将开发用于构建多语言软件的原则性软件工具链。该项目的新颖性包括(1)设计语言扩展，允许程序员通过一种称为链接类型的机制，指定他们希望如何与语言中缺少的概念功能进行互操作(或链接)，以及(2)开发编译器，正式保证程序员在源代码级别所做的任何推理在编译到目标后都是合理的。该项目有可能对软件开发环境产生巨大影响，因为它将允许程序员使用一种接近他们问题领域的语言，并为他们提供软件工具链，使其能够轻松地将以不同语言编写的组件组合成多语言软件系统。该项目将评估链接类型的想法，方法是用链接类型扩展ML以与Rust交互，Rust是一种具有一流控制的语言和标准化语言，并将类型保持编译器开发为通用的类型化LLVM目标语言。该项目将设计一种富依赖类型的类似LLVM的目标语言，可以封装来自不同源语言的效果，以支持从这些语言进行完全抽象的编译。该项目还将调查跨语言类型错误的报告，以帮助程序员在编写以不同语言编写的组件时。这一奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

When building large software systems, programmers should be able to use the best language for each part of the system. But when a component written in one language becomes part of a multi-language system, it may interoperate with components that have features that don't exist in the original language. This affects programmers when they refactor code (i.e., make changes that should result in equivalent behavior). Since programs interact after compilation to a common target, programmers have to understand details of linking and target-level interaction when reasoning about correctly refactoring source components. Unfortunately, there are no software toolchains available today that support single-language reasoning when components are used in a multi-language system. This project will develop principled software toolchains for building multi-language software. The project's novelties include (1) designing language extensions that allow programmers to specify how they wish to interoperate (or link) with conceptual features absent from their language through a mechanism called linking types, and (2) developing compilers that formally guarantee that any reasoning the programmer does at source level is justified after compilation to the target. The project has the potential for tremendous impact on the software development landscape as it will allow programmers to use a language close to their problem domain and provide them with software toolchains that make it easy to compose components written in different languages into a multi-language software system.The project will evaluate the idea of linking types by extending ML with linking types for interaction with Rust, a language with first-class control, and a normalizing language, and developing type preserving compilers to a common typed LLVM-like target language. The project will design a rich dependently typed LLVM-like target language that can encapsulate effects from different source languages to support fully abstract compilation from these languages. The project will also investigate reporting of cross-language type errors to aid programmers when composing components written in different languages.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.