Magazine: Profile Armando Solar-Lezama
Profile Armando Solar-Lezama
Full text also available in the ACM Digital Library as PDF | HTML | Digital Edition
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
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee.
The Digital Library is published by the Association for Computing Machinery. Copyright © 2010 ACM, Inc.
To comment you must create or log in with your ACM account.
JERIC is an electronic publication providing access to high quality, archival resources suitable for use in support of computing education
Forum on all aspects of the Ada language and technologies
Explores programming language concepts and tools focusing on design, implementation, and efficient use
TALG publishes original research of the highest quality dealing with algorithms that are inherently discrete and finite, and having mathematical content in a natural way
The purpose of TOPLAS is to present research results on all aspects of the design, definition, implementation, and use of programming languages and programming systems
TWEB is a journal publishing refereed articles reporting the results of research on Web content, applications, use, and related enabling technologies
ACM's flagship magazine, Communications of the ACM, is the premier chronicler of computing technologies, covering the latest discoveries, innovations, and research that inspire and influence the field
JETC covers research and development in emerging technologies in computing system
Support Vector Machine: a machine learning methodology for classifying data into two categories, based on a round of supervised training