National Science Foundation, Intel and Microsoft
What computational technologies support programmers in the task of building complex systems? So far, four technologies have been adopted: testing, type checking, model checking, and compilers. First three focus on assuring correctness of code; compilers actually help with writing the code, by raising the level of programming abstractions. Despite adoption of high-level languages, though, it is fair to say that we don't know how to usefully burn computer cycles at the frontend of the program development process: programmers still rely on paper and pencil when writing code. We are developing computer-aided programming that brings the computational power to the process of constructing programs. We pose the problem as synthesis of programs from multi-modal specifications: templates of programs, declarative assertions, executable specifications, examples and demonstrations. We are developing synthesis theories and algorithms, language constructs and tools that embed synthesis into the programming process.