Guaranteed Code

Adam Chlipala, an associate professor of computer science at MIT, thinks there’s a better way to write computer programs.

Most programs just list operations that the computer should perform when it receives particular types of data. The programmer has to write tests to determine whether a program does what it’s supposed to, and since it’s virtually impossible to predict all the ways a program might be used, most software has bugs.

Chlipala prefers so-called functional programming. Instead of stringing together imperative commands, a functional programmer defines a set of functions, or mathematical relationships between inputs and outputs. Essentially, functional programming expresses what a program does as a set of equations.

Thinking of programs as combinations of functions can be unintuitive, “but for the people it works for, it’s really an amazing productivity enhancer,” Chlipala says. For one thing, it can eliminate testing. Functional programs are so mathematically precise that it’s relatively simple to verify them, or prove that they do what they should, automatically.

One of Chlipala’s chief research interests is broadening the scope of automatic verification. For instance, verification tools that he and colleagues developed made it possible to create the first file system—the part of an operating system that governs data storage—guaranteed not to lose program data during a system crash.

Another advantage of functional languages is that they eliminate a lot of the grunt work from programming. Again, because functional programs are so precise, it’s easy for compilers—the programs that turn code into executable files—to figure out how to make them run most efficiently.

One of Chlipala’s most popular tools is a functional language called Ur/Web—the only programming language that lets programmers specify all of a Web application’s functionality in a single program. Ur/Web’s compiler then automatically generates the XML code, JavaScript code, and database queries necessary to implement the application. It also ensures that these different components interact correctly.

Ur/Web is similar to other functional languages, but it adds security features that enable it to automatically plug holes common in Web applications. For instance, it can guarantee that a bit of its code imported into one section of a page (such as an advertisement) can’t spy on another (such as a calendar tool).

Like many computer scientists in their 30s, Chlipala had tried his hand at writing video games in high school. But that enterprise quickly took him in a different direction. When he was a freshman, his attempts to write games for Texas Instruments’ graphing calculator led him to develop a compiler for the device.

He continued to focus on compilers as an undergraduate at Carnegie Mellon University, and in his first semester as a graduate student at the University of California, Berkeley, his future thesis advisor asked him if he’d like to contribute to a project on computer-aided verification. Chlipala was immediately hooked.

“There is a certain kind of paranoid personality that gets addicted to this kind of work, and that’s definitely me,” he says. “There aren’t many things that are absolutely sure in this world, but when you do machine-checked proofs about programs, you get pretty close.”