Massive compute power has long been available to us but we need more ideas on how to harness it in programming. While testing and verification dutifully number-crunch programs, they do not fix the bugs they find. Moving closer to programmers, recent tools have become true cognitive assistants: search engines find relevant code samples, verifiers explain bugs, and software miners discover properties absent in the documentation. Still, these tools do not directly address the problem of writing programs.

This talk will describe a growing family of programmer tools that assist in writing programs. Their premise is that programs can be decomposed into insight and mechanics, and that the later can be synthesized from the former. The first research problem is how to describe the insight without spelling out the details. I will describe the idea of sketching (programs with holes) and how we move beyond programming by demonstration by asking an oracle for a demonstration. The second problem is how to synthesize the program from the insight. Some of our tools combine mining of examples with program analysis, and some rely on recent advances in decision procedures, such as SAT, that combine search with algebraic reasoning. I will conclude with open problems motivated by some of our more ambitious ideas.