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