EAGER: Human-Centered Software Synthesis

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

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.