Making it Easier to Program and Protect the Web

A Heart for System Infrastructure
As he was growing up in the Lehigh Valley region of Pennsylvania, programming became “an important part of my self-identity,” Chlipala says. In the late 1980s, when Chlipala was young, his father, a researcher who ran physics experiments for AT&T Bell Laboratories, taught him some basic programming skills. He quickly became hooked.

In the late 1990s, when the family finally connected to the internet, Chlipala had access to various developer resources that helped him delve “into more serious stuff,” meaning designing larger, more complex programs. He worked on compilers — programs that translate programming language into machine-readable code — and web applications, “when apps were an avant-garde subject.”  

In fact, apps were then called “CGI scripts.” CGI is an acronym for Common Gateway Interface, which is a protocol that enables a program (or “script”) to talk to a server. In high school, Chlipala and some friends designed CGI scripts that connected them in an online forum for young programmers. “It was a means for us to start building our own system infrastructure,” he says.

And as an avid computer gamer, the logical thing for a teenaged Chlipala to do was design his own games. His first attempts were text-based adventures coded in the BASIC programming language. Later, in the C programming language, he designed a “Street Fighter”-like game, called Brimstone, and some simulated combat tabletop games.

It was exciting stuff for a high schooler. “But my heart was always in systems infrastructure, like code compilers and building help tools for old Windows operating systems,” Chlipala says.

From then on, Chlipala worked far in the background of web services, building the programming foundations for developers. “I’m several levels of abstraction removed from the type of computer programming that’s of any interest to any end-user,” he says, laughing.

Impact in the Real World
After high school, in 2000, Chlipala enrolled at Carnegie Melon University, where he majored in computer science and got involved in a programming language compiler research group. In 2007, he earned his PhD in computer science from University of California at Berkeley, where his work focused on developing methods that can prove the mathematical correctness of algorithms.

After completing a postdoc at Harvard University, Chlipala came to MIT in 2011 to begin his teaching career. What drew Chlipala to MIT, in part, was an opportunity “to plug in a gap, where no one was doing my kind of proofs of computer systems’ correctness,” he says. “I enjoyed building that subject here from the ground up.”

Testing the source code that powers web services and computer systems today is computationally intensive. It mostly relies on running the code through tons of simulations, and correcting any caught bugs, until the code produces a desired output. But it’s nearly impossible to run the code through every possible scenario to prove it’s completely without error.

Chlipala’s research group instead focuses on eliminating the need for those simulations, by designing proven mathematical theorems that capture exactly how a given web service or computer system is supposed to behave. From that, they build algorithms that check if the source code operates according to that theorem, meaning it performs exactly how it’s supposed to, mostly during code compiling.

Even though such methods can be applied to any application, Chlipala likes to run his research group like a startup, encouraging students to target specific, practical applications for their research projects. In fact, two of his former students recently joined startups doing work connected to their thesis research.  

One student is working on developing a platform that lets people rapidly design, fabricate, and test their own computer chips. Another is designing mathematical proven systems to ensure the source code powering driverless car systems doesn’t contain errors that’ll lead to mistakes on the road. “In driverless cars, a bug could literally cause a crash, not just the ‘blue-screen death’ type of a crash,” Chlipala says.

Now on sabbatical from this summer until the end of the year, Chlipala is splitting his time between MIT research projects and launching his own startup based around tools that help people without programming experience create advanced apps. One such tool, which lets nonexperts build scheduling apps, has already found users among faculty and staff in his own department. About the new company, he says: “I’ve been into entrepreneurship over the last few years. But now that I have tenure, it’s a good time to get started.”

Rob Matheson is writer and web producer at MIT News. Reprinted with permission of MIT News