PROFILE

Armando Solar-Lezama
Programming Machines to
Program Bits
BY MICHAEL BERNS TEIN
DOI: 10.1145/1836543.1836556

It’s the rare programmer who doesn’t get frustrated by her own code. Bugs are tough to pinpoint, race conditions produce unpredictable results, and performance tweaks means rewiring large blocks of code.

For most programmers, these situations are just a fact of life. Others are a bit more introspective, recognizing when they tend to make the same errors over and over.

And a select few of those intend to do something about it. Professor Armando Solar-Lezama is one of them.

Solar-Lezama is a programming systems researcher at the Massachussets Institute of Technology’s Computer Science and Artificial Intelligence Lab (CSAIL), and a recent Ph.D. graduate from University of California-Berkeley. If he gets his way, you will be programming more complex systems with less hassle. His modus operandi is to use automation and reasoning to support difficult programming problems. For example, his graduate research let programmers specify a sketch of an implementation, and used a program synthesizer to transform the sketch into a full and correct implementation.

In his most recent work, Solar-Lezama is thinking about large codebases. “The programming problem is no longer, ‘How do I do this from scratch?’ It’s, ‘ Where can I find all the components that I’m sure are out there to do all these different pieces of the task, and how do I get them to talk to each other?” he says.

Even when the platform is carefully engineered and extensible, like the Eclipse platform, it’s still absolutely a pain to insert new code into the system. Solar-Lezama aims to extend IDEs beyond their current superficial understanding of types and names to support new code injection into an existing large-scale software system.

Though Solar-Lezama is looking to the future, his recent time in graduate school gives him an interesting perspective on research methodology. Transitioning into a faculty position at a number one computer science department isn’t easy, but he thinks the larger change actually occurs during graduate school. He winces a bit at the memory of it.

“Very early in my graduate student career, I got so passionate about the details of the research. It’s very easy to lose the big picture perspective of where the research is going and where [you] want to take it. Then you crack the problem and realize… now what?” he says. The maturing comes not when a researcher moves out of low-level issues (he would argue that that shift rarely happens) but when he or she becomes more agile in moving up and down the conceptual ladder, from low-level implementation to big picture directions.

What brought the MIT professor to research in programming systems? He was originally a nuclear engineer, he explains, but shifted to computer science after a particular experience as a freshman in college. A lecturer mentioned in passing that nobody knew whether it was possible to solve the Traveling Salesman problem in polynomial time, “and I thought, nah, that can’t be right,” Solar-Lezama remembers. After 10 consecutive all-nighters, he still hadn’t actually solved the NP-complete problem (or he wouldn’t have needed graduate school to land that MIT professorship), but it was enough to get him hooked.

Questions that were fading when he took on his ill-fated
battle against P vs. NP are now returning to prominence. “For
a while, computers got faster than we really needed them to
be. We could just count on Moore’s law and pile in the layers of
abstraction, worry about issues like programmability and move
responsibilities to the runtime system.”
However, with the coming of age of hand-held devices and
limited battery life, performance and power matter again.
Solar-Lezama wants to leverage programmers’ creativity and
insight in solving these problems, but thinks it will be important
to separate functionality from performance where possible. He
explains, “What you really want are programming technologies
that let you say, ‘On one hand, this is what my program needs
to do. Separately, these are the cool tricks you should be
using to get the performance.’” Then, rather than write a
dozen different versions of a system for states like plugged-
in activity, battery-driven activity, and low-battery activity,
a program synthesizer can combine the constraints and the
tricks to produce an on-demand version of the program. Of
course, testing then becomes exponentially harder, but the
synthesizer can tell the programmer which situations to
test in order to encounter possible interactions, and can use
equivalence checking to make sure that two versions of the
code are functionally equivalent.

In this way, Solar-Lezama hopes to bind theoretical work like equivalence checking with pragmatic considerations like power consumption. He has a streak of creativity that suggests he’ll succeed, too. As a graduate student, he once wired an entire concolic automated test generation tool using the text processing utility Awk. So next time you wish you could program better, keep in mind that Solar-Lezama is working on it, although you might need to install Awk to use it.

© 2010 ACM 1528-4972/10/0900 $10.00