EAGER: Human-Centered Software Synthesis

该项目正在开发一种新的编程模型，简化了复杂的低级系统代码的开发。在新模型中，程序员首先提供简单的图表和动画，展示实现背后的一些高级见解。在与用户交互以澄清任何潜在的遗漏或不一致之后，系统自动导出正确的实现。 这些交互旨在暴露程序员推理中的漏洞，并以图表、不变量或简单单元测试的形式捕获新的见解。因此，该工具可以帮助程序员实现一个更好的理解的问题，除了提供一个implementation.The新的编程模型是由一个新品种的软件合成算法的工作框架的合成问题作为一个约束满足问题的支持。在这种方法中，程序员提供的不同形式的输入被独立地转换为约束。在高层次上，该方法相当简单;挑战在于为程序和约束找到有效的表示。 图形化的形式主义由于其许多遗漏而特别提出了一些有趣的问题，但是抽象解释和需求驱动的约束生成的组合使这个问题变得易于处理。新的编程模型体现了以人为中心的综合方法，可以改变开发复杂系统代码的方式，并且可以为新一代的编程工具指明道路，这些工具将联合收割机形式化方法与HCI结合起来，使编程更容易、更可靠。

This project is developing a new programming model that simplifies the development of complex low-level system's code. In the new model, the programmer starts by providing simple diagrams and animations showing some of the high-level insight behind an implementation. After interacting with the user to clarify any potential omissions or inconsistencies, the system automatically derives a correct implementation. The interactions are designed to expose gaps in the programmer's reasoning, and to capture new insights in the form of diagrams, invariants, or simple unit tests. As a result, the tool helps the programmer achieve an improved understanding of the problem in addition to delivering an implementation.The new programming model is supported by a new breed of software synthesis algorithms that work by framing the synthesis problem as a constraint satisfaction problem. In this approach, the different forms of input provided by the programmer are independently translated into constraints. At the high-level, the approach is fairly simple; the challenge lies in finding efficient representations for both the program and the constraints. The graphical formalisms in particular pose some interesting problems due to their many omissions, but a combination of abstract interpretation and demand-driven constraint generation make this problem tractable.The new programming model embodies a human-centered approach to synthesis that could transform the way complex pieces of systems code are developed, and could show the way for a new generation of programming tools that combine formal methods with HCI to make programming easier and more reliable.