SHF: MEDIUM: Performant Sound Gradual Typing

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

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.