CAREER: Foundations and Applications of Constraint-based Synthesis

程序合成承诺通过根据更自然和更容易理解的用户提供的规范自动生成乏味的、容易出错的代码，从而使大众编程大众化。在过去的二十年里，计算能力的进步导致了程序合成技术的激增，这些技术涉及从逻辑、编程语言理论和机器学习的各个领域。这些技术在操作方式上有很大的不同，没有一种技术在所有情况下都是普遍优越的。此外，对用户对合成器等高级开发工具的实际需求和情感了解甚少，这不可避免地导致了理论上有趣但最终不具说服力或不切实际的工具的开发。这个项目的新颖性有两个：(A)为这些不同的技术提供了一个统一的框架，以便更好地理解它们的理论基础，并可以在该框架的基础上构建下一代程序合成工具，以及(B)确定在制作程序合成工具时应该考虑的一组人的因素。这个项目的最终影响是，不仅在技术方面，而且在学科方面统一了程序合成的观点：编程语言、人机交互和计算机科学教育。该项目集中在两个主要努力上。第一种是基于广义的约束概念开发用于综合的统一的语义基础集，所述广义约束概念捕获利用当前技术发现的规范的常见形式，例如类型、示例、逻辑约束、句法约束和部分程序。这种基于约束的综合方法自然会产生一种演绎的、孔引导的编程风格，与传统的编程模型不同。因此，该项目的第二项工作是对开发人员对这种编程风格的需求和情感进行系统研究，并基于这些结果设计下一代开发工具。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.