SHF: Medium: Formal Methods as a First-Class Citizen of a Mainstream Compiler Framework

编译器和类似编译器的工具一直是实现高程序员生产力的重要组成部分。由于大数据、机器学习和人工智能等新应用领域的激增，推动了新硬件和新编程语言的发展，现在尤其如此。该项目开发了一种称为多级中间表示（MLIR）的开源编译器基础设施，它承诺通过从相对简单的高级规范自动生成一些最繁琐和最容易出错的编译器代码，从而使编译器和类似编译器的工具更容易构建。MLIR支持创建特定于领域的方言，这样就可以用它来解决不同类型的问题。该项目探讨了如何使开发人员能够实现新的MLIR方言，从而正式指定方言中操作的含义，以便支持自动生成重要工具，如解释器、优化器和翻译验证器，这些工具使用自动定理证明器来显示优化编译器没有出错。该项目更广泛的议程是在一个重要的开源编译器工具链中推动编译的数学基础付诸实践，这样正式方法驱动的软件开发的好处就可以影响到大量的用户。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Compilers and compiler-like tools have always been an important part of achieving high programmer productivity. This is especially true now due to the proliferation of new application domains, such as big data, machine learning, and AI, that are spurring the development of new hardware and new programming languages. This project develops an open-source compiler infrastructure, called multi-level intermediate representation (MLIR), that promises to make compilers and compiler-like tools easier to build by automatically generating some of the most tedious and error-prone kinds of compiler code from a relatively simple, high-level specification. MLIR supports the creation of domain-specific dialects so that it can be used to solve different kinds of problems. The project explores how to enable developers implementing a new MLIR dialect to formally specify the meaning of operations in the dialect, in order to support automated generation of important tools such as interpreters, optimizers, and translation validators, which use an automated theorem prover to show that an optimizing compiler did not make any mistakes. The project's broader agenda is to push the mathematical foundations of compilation into practice, in an important open-source compiler toolchain, so that the benefits of formal-methods-driven software development can impact a large number of users.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.