CRII: SHF: RUI: Exploring Human-in-the-loop Program Synthesis Through Live Coding

程序综合是一种正式的技术，它承诺降低软件开发成本，降低软件错误的风险，并使编程技能更容易为更广泛的受众所接受。然而，对于这一领域的所有理论和技术的发展，用户对程序合成的采用一直受到限制。扩展合成影响的一个关键障碍是完全自动化的软件合成与实践中使用的迭代软件设计过程不匹配。大多数现有技术都努力实现完全自动化，充当用户的黑盒：用户提供规范，工具返回完整的程序代码。研究人员建议通过人在循环合成来克服这一障碍，这种合成允许用户通过与合成引擎的交互来逐步完善规范和代码。该项目侧重于开发技术和理论，以增加在现实世界系统中程序综合的采用。他们使用了一种来自计算机音乐社区的表演实践，称为“现场编码”，在这种实践中，用户编写代码，实时生成音乐（或其他媒体）。本项目形式化了人机循环程序合成及其与实时编码的交叉，并开发了新的人机循环程序合成技术。调查人员探索了这些技术在实时编码和其他设置中的使用。该项目还将为女性本科生提供参与计算机科学研究的机会，其中许多人是第一次参与。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Program synthesis is a formal technique that promises to decrease software development costs, decrease the risk of software bugs, and make programming skills more accessible to a broader audience. Yet for all the development of theory and techniques in this area, the adoption of program synthesis by users has been limited. A key hurdle in expanding the impact of synthesis is that fully automated software synthesis does not match the iterative software design process that is used in practice. The majority of existing techniques strive to be fully automated, acting as black-boxes for users: the user provides a specification and the tool returns complete program code. The investigators propose to overcome this hurdle through human-in-the-loop synthesis which allows a user to incrementally refine specifications and code through interaction with the synthesis engine. This project focuses on developing techniques and theories that increase the adoption of program synthesis in real-world systems. They use a performative practice from the computer-music community, called Live Coding, in which users write code that generates music (or other media) in real-time. This project formalizes human-in-the-loop Program Synthesis and its intersection with Live Coding, and develops new human-in-the-loop program-synthesis techniques. The investigators explore the use of these techniques in Live Coding and other settings. This project will also provide the opportunity for female undergraduates to participate in computer-science research - many for the first time.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.