SHF: MEDIUM: Performant Sound Gradual Typing

Indiana University, Bloomington IN

Investigators

Abstract

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.