Skip to Content
MIT News feature

Guaranteed Code

Adam Chlipala is building a programming platform that could generate bug-free software.
October 24, 2017
Ariel Davis

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.”

Keep Reading

Most Popular

This new data poisoning tool lets artists fight back against generative AI

The tool, called Nightshade, messes up training data in ways that could cause serious damage to image-generating AI models. 

Rogue superintelligence and merging with machines: Inside the mind of OpenAI’s chief scientist

An exclusive conversation with Ilya Sutskever on his fears for the future of AI and why they’ve made him change the focus of his life’s work.

The Biggest Questions: What is death?

New neuroscience is challenging our understanding of the dying process—bringing opportunities for the living.

Driving companywide efficiencies with AI

Advanced AI and ML capabilities revolutionize how administrative and operations tasks are done.

Stay connected

Illustration by Rose Wong

Get the latest updates from
MIT Technology Review

Discover special offers, top stories, upcoming events, and more.

Thank you for submitting your email!

Explore more newsletters

It looks like something went wrong.

We’re having trouble saving your preferences. Try refreshing this page and updating them one more time. If you continue to get this message, reach out to us at with a list of newsletters you’d like to receive.