SHF: Small: Collaborative Research: Semantic Foundations for Hole-Driven Development

University Of Colorado At Boulder, Boulder CO

Investigators

Abstract

Software developers today spend much of their time editing programs that are missing pieces or that contain transient errors of various sorts. Conventional language definitions are silent about programs with "holes" like these. As a result, current development tools resort to ad hoc heuristics that fail to provide precise, accurate feedback about the program exactly when the developer needs it most. To tackle the problem of programs with holes directly, the project's novelties are to provide (1) a principled mathematical characterization of programs with holes, and (2) an open source development environment called Hazel designed from the ground up to support hole-driven development. The project's impacts are that (1) Hazel will initially target CS instructors, students, and domain scientists working in STEM fields, all of whom stand to benefit from more precise, live feedback throughout the development process; and (2) the theoretical foundations and prototype will inform the design of other software development environments both in research and industry, much like programming language theory has had a major impact on programming language and compiler design in the past decades. By applying the rigorous methodology of programming language theory to problems in programming environment design, the project will open up substantial new research directions for semanticists and tool designers alike. This project has several related specific aims that support the practice and (currently under-developed) theory of interactive software development. These aims are connected by a common technical device: Typed Holes. Specifically, the project will develop (1) a static semantics for typed holes, (2) a dynamic semantics for live programming with typed holes, (3) a semantics for structured edit actions that insert typed holes automatically, and (4) a mechanism that uses typed holes to support programming by direct manipulation of graphical user interfaces inside the program editor. 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.