SHF: MEDIUM: Performant Sound Gradual Typing

在过去的二十年里，软件开发人员已经转向了一种新的计算机语言。虽然这些语言提高了开发人员的生产力，并允许他们为新设备创建软件，但它们也有一个明显的缺点，即没有预先检查足够的安全属性。一旦部署了软件，故障就会出现，可能会损害客户的利益。研究人员最近通过创造混合语言解决了这个问题，混合语言包括快速生产和逐步增加安全检查的方法，而工业开发人员则开发了完全忽略安全的混合语言。该项目的新奇之处在于这些混合语言的性能，正如最近发现的那样，这些混合语言阻止了它们的采用。如果成功，该项目的影响可能会大规模改变现代软件开发的格局，为最常见的快速软件生产的现代方法增加安全性。研究项目解决了提高这些混合语言的性能的具体问题。虽然先前的研究表明，混合编程语言确实是软件开发人员可能想要的灵活媒介，但它也揭示了这些语言存在严重的性能问题。因此，该项目探索了如何消除这些性能瓶颈的四个不同的想法：(1)原则性地放松安全保证；(2)专门针对额外的安全检查调整的编译器技术；(3)减少这些检查所需的内存；(4)应用软件验证技术。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Over the past two decades, software developers have switched to a new breed of computer languages. While these languages increase the developers' productivity and allow them to create software for novel devices, they also have the distinct disadvantage of not checking enough safety properties upfront. Failures show up once the software is deployed and may hurt customers. Researchers have recently addressed this problem with the creation of hybrid languages, which embrace rapid production and a way to add safety checks gradually, while industrial developers have developed hybrid languages that omit safety entirely. The project's novelties are about the performance of these hybrid languages, which, as recently discovered, prevent their adoption. If successful, the project's impacts are likely to change the landscape of modern software development on a large scale, adding safety to the most common modern approach to rapid software production.The research project addresses the specific problem of improving the performance of these hybrid languages. While prior research demonstrates that hybrid programming languages are indeed the flexible medium that software developers may want, it also reveals significant performance problems with these languages. The project therefore explores four different ideas of how to eliminate these performance bottlenecks: (1) principled relaxation of the safety guarantees; (2) compiler technology specifically tuned to the additional safety checks; (3) reduction of memory needed for these checks; and (4) application of software verification technology.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.