Emina Torlak Clojure/West 2017 Interview
Emina Torlak will be giving a talk at Clojure/West 2017. She will be speaking about Rosette.
Follow her on her Homepage and GitHub.
PurelyFunctional.tv: How did you get into functional programming?
Emina Torlak: My first undergraduate course in computer science (6.001 at MIT) was taught in Scheme. Until then, I had only programmed in rather low-level imperative languages: Basic, Pascal, and C. Learning Scheme was an amazing and eye-opening experience. I was like a kid in a candy store! We implemented our own object-oriented system from scratch and, eventually, our own metacircular interpreter. This was easily one of the best and most memorable courses I have ever taken.
PF.tv: What is your talk about?
ET: I will be talking about Rosette, a new functional language for creating programming tools backed by powerful automated reasoning engines. Rosette extends Racket with a few constructs that make it easy for anyone to build advanced tools for program verification and synthesis. Building these tools usually takes months or years of work, as well as expertise in many fields, from formal methods to programming languages to software engineering. With Rosette, creating such a tool is as easy as defining a new domain-specific language in Racket. Once you define your language, you get the tools for (almost) free. I will show you how to use Rosette and how it works, concluding with a whirlwind tour of recent applications to finding bugs in radiation therapy software, generating efficient code for ultra low-power hardware, and creating custom tutors for K-12 algebra.
PF.tv: Who is your talk for?
ET: All programmers who are curious about automated reasoning tools, how they can help you write better code, and how you can build your own tools without having to become an expert in automated reasoning!
PF.tv: What do you hope people will take away from the talk?
ET: The last few decades have brought enormous advances in programming tools that are backed by powerful automated reasoning engines. These tools are already being used to find security bugs in major software products, to build verified kernels, and to superoptimize LLVM IR. The goal of this talk is to raise awareness of the potential of these tools to revolutionize everyday programming: we are working on a future in which all programmers will have the means to rapidly create custom automation for tasks they care about.
PF.tv: What concepts do you recommend people be familiar with to maximize their experience with the talk?
ET: Basic knowledge of Racket or another LISP-like language would be great. Some familiarity with creating domain-specific languages (DSLs) by writing libraries or interpreters would be a plus (though not required).
PF.tv: What resources are available for people who want to study up before the talk?
ET: You can find out more about solver-aided programming, the Rosette language, and applications at emina.github.io/rosette. If you are curious about how it all works, this paper describes the underlying technology in detail.
PF.tv: Where can people follow you online?
PF.tv: Are there any projects you'd like people to be aware of? How can people help out?
ET: We are always excited to see new applications of Rosette. We'd love for more people to try it out, use it to solve a problem they care about, and tell us about it! And if Rosette doesn't work for you, we want to hear about that too. Our long-term goal is to make solver-aide d programming as natural and easy to use as possible, and in my experience, this is best done by interacting with users and actively supporting their needs.
PF.tv: Where do you see the state of functional programming in 10 years?
ET: I expect functional programming to become a key part of every programmer's toolbox in 10 years. Many successful programming paradigms are already functional, from general-purpose frameworks such as map-reduce to high-performance domain-specific languages (DSLs) such as Halide. In fact, most DSLs targeted by program synthesis tools (for example, FlashFill) are also functional. This trend will undoubtedly continue: as the complexity of the systems we build increases, so does the need for high-level languages that are easy for people to use and for automated tools (such as verifiers, optimizers, and synthesizers) to reason about.
PF.tv: If functional programming were an animal, what animal would it be?
ET: A cat! Clever, effective, sleek, and beautiful.