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

SHF：小型：协作研究：空洞驱动开发的语义基础

• 批准号: 1814900
• 负责人: Ravi Chugh
• 金额: $ 24.68万
• 依托单位: University of Chicago
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-10-01 至 2021-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1814900&HistoricalAwards=false
• 关键词: SHF; Small; Collaborative; Research; Semantic

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.

如今，软件开发人员花费大量时间来编辑缺少部分或包含各种瞬态错误的程序。传统的语言定义对带有此类“漏洞”的程序只字不提。因此，当前的开发工具采用临时启发式方法，无法在开发人员最需要的时候提供有关程序的精确、准确的反馈。为了直接解决有漏洞的程序问题，该项目的新颖之处在于提供（1）有漏洞的程序的原则性数学特征，以及（2）一个名为 Hazel 的开源开发环境，该环境是从头开始设计的，用于支持漏洞驱动的开发。该项目的影响是：(1) Hazel 最初将针对计算机科学教师、学生和在 STEM 领域工作的领域科学家，他们所有人都将在整个开发过程中从更精确、实时的反馈中受益； (2) 理论基础和原型将为研究和工业中的其他软件开发环境的设计提供信息，就像编程语言理论在过去几十年中对编程语言和编译器设计产生了重大影响一样。该项目将编程语言理论与编程环境设计中的问题结合起来，将为语义学家和工具设计者等开辟大量新的研究方向。该项目有几个相关的具体目标，支持交互式软件开发的实践和（目前尚未开发的）理论。这些目标通过一个通用的技术装置连接起来：类型孔。具体来说，该项目将开发（1）用于类型孔的静态语义，（2）用于使用类型孔进行实时编程的动态语义，（3）用于自动插入类型孔的结构化编辑操作的语义，以及（4）一种机制它使用类型孔通过在程序编辑器内直接操作图形用户界面来支持编程。该奖项反映了 NSF 的法定使命，并且通过使用基金会的智力优点和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Filling Typed Holes with Live GUIs

使用实时 GUI 填充键入的孔

• DOI: 10.1145/3453483.3454059
• 发表时间: 2021
• 期刊: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
• 作者: Omar, Cyrus;Moon, David;Blinn, Andrew;Voysey, Ian;Collins, Nick;Chugh, Ravi
• 通讯作者: Chugh, Ravi

Live functional programming with typed holes

带类型孔的实时函数式编程

• DOI: 10.1145/3290327
• 发表时间: 2019
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Omar, Cyrus;Voysey, Ian;Chugh, Ravi;Hammer, Matthew A.
• 通讯作者: Hammer, Matthew A.

Program sketching with live bidirectional evaluation

通过实时双向评估进行程序草图绘制

• DOI: 10.1145/3408991
• 发表时间: 2020
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Lubin, Justin;Collins, Nick;Omar, Cyrus;Chugh, Ravi
• 通讯作者: Chugh, Ravi