Programming for Everyone: From Solvers to Solver-Aided Languages and Beyond Emina Torlak ( University of California, Berkeley ) Monday, March 31, 4:30pm Computer Science 105 We live in a software-driven world. Software helps us communicate and collaborate; create art and music; and make discoveries in biological, physical, and social sciences. Yet the growing demand for new software, to solve new kinds of problems, remains largely unmet. Because programming is still hard, developer productivity is limited, and so is end-users' ability to program on their own. In this talk, I present a new approach to constructing programs, which exploits advances in constraint solving to make programming easier for experts and more accessible to everyone else. The approach is based on two observations. First, much of everyday programming involves the use of domain-specific languages (DSLs) that are embedded, in the form of APIs and interpreters, into modern host languages (for example, JavaScript, Scala or Racket). Second, productivity tools based on constraint solvers (such as verification or synthesis) work best when specialized to a given domain. Rosette is a new kind of host language, designed for easy creation of DSLs that are equipped with solver-based tools. These Solver-Aided DSLs (SDSLs) use Rosette's symbolic virtual machine (SVM) to automate hard programming tasks, including verification, debugging, synthesis, and programming with angelic oracles. The SVM works by compiling SDSL programs to logical constraints understood by SMT solvers, and then translating the solver's output to counterexamples (in the case of verification), traces (in the case of angelic execution), or code snippets (in the case of synthesis and debugging). Rosette has hosted several new SDSLs, including imperative SDSLs for data-parallel and spatial programming; a functional SDSL for specifying executable semantics of secure stack machines; and a declarative SDSL for web scraping by example. Emina Torlak is a researcher at U.C. Berkeley, working at the intersection of software engineering, formal methods, and programming languages. Her focus is on developing tools that help people build better software more easily. She received her B.Sc. (2003), M.Eng. (2004) and Ph.D. (2009) from MIT, where she developed Kodkod, an efficient SAT-based solver for relational logic. Kodkod has since been used in over 70 tools for verification, debugging, and synthesis of code and specifications. Emina has also worked on a wide range of domain-specific formal methods. She won an ACM SIGSOFT distinguished paper award for her work at LogicBlox, where she built a system for synthesizing massive data sets, used in testing of decision support applications. As a member of IBM Research, she led the development of a tool for bounded verification of memory models, enabling the first fully automatic analysis of the Java Memory Model. These experiences inspired her current research on solver-aided languages, which aims to reduce the effort of applying formal methods to new problem domains.