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

点击翻译按钮获取中文摘要

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.