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.
This project explored new directions in software synthesis---the use of computing power to help programmers write software. In order for the computer to help programmers write software, the machine needs to be told about the programmer's intent, and this is one of the big challenges in this field: describing the programmer's intent clearly and unambiguously in terms that a machine can understand can be just as hard as writing a program. The goal for this project was to explore new forms of interaction between the programmer and the software synthesizer that allowed programmers to easily offload some of the effort of programming to a synthesis tool. Intellectual Merit: The main contribution of this work was to demonstrate a new technique that allows programmers to communicate their intent in ways that mimic the formalisms they use to communicate with each other. Specifically, we showed that we could automatically synthesize non-trivial pieces of code from textual descriptions of diagrams like the ones programmers use to describe a complicated algorithm on a whiteboard. These diagrams usually describe the behavior of the algorithm on some sample input; making sense of these diagrams, therefore, requires piecing together insights from different examples and generalizing from them. This work was published in the 2011 ACM Symposium on the Foundations of Software Engineering. Our work also explored a different way for programmers to interact with a synthesis engine in the context of a large existing piece of software. We found that when working with big software frameworks, programmers sometimes know that they need two components to interact with each other, but they don't know how to get these two components to work together. We found that given the names of the two components in question, it is possible to automatically find how to get them to interact by automatically analyzing how they are used in other places within the framework. The MIT news office produced a nice piece about this work which can be found here: http://web.mit.edu/newsoffice/2011/object-oriented-oracle-1007.html The results were also published in the 2011 ACM sponsored OOPSLA-SPLASH conference. Broader Impact: The main impact of our tool work will be in improving programmer productivity. For example, in a controlled user study, we found that one of the prototypes we developed for this project could increase programmer productivity by close to 50%.
