CAREER: Foundations and Applications of Constraint-based Synthesis

点击翻译按钮获取中文摘要

Program synthesis promises to democratize programming for the masses by automating the generation of tedious, error-prone code from more natural and understandable user-provided specification. Over the past two decades, advances in computational power have led to a proliferation of program-synthesis techniques that draw upon various fields ranging from logic, programming-language theory, and machine learning. These techniques differ substantially in how they operate, and no single technique is universally superior in all cases. Furthermore, little is understood about users' actual needs and sentiment towards advanced development tools like synthesizers, which inevitably leads to the development of theoretically interesting but ultimately uncompelling or impractical tools. The novelties of this project are two-fold: (a) providing a unifying framework for these differing techniques so that their theoretical underpinnings can be better understood and next-generation program synthesis tools can be built on top of this framework, and (b) identifying the set of human factors that should be considered when making program-synthesis tools. This project's impact is, ultimately, unifying perspectives on program synthesis not just in terms of techniques but also disciplines: programming languages, human-computing interaction, and computer-science education.The project focuses on two primary efforts. The first is developing a unified set of semantic foundations for synthesis based on a generalized notion of constraint that captures the common forms of specifications found with current techniques, e.g., types, examples, logical constraints, syntactic constraints, and partial programs. This constraint-based approach to synthesis naturally leads to a deductive, hole-guided programming style, different from traditional programming models. Therefore, the project's second effort is a systematic study of the needs and sentiment of developers towards this style of programming and the design of next-generation development tools based on these results.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.