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

computation concept
computation concept

How AI is reinventing what computers are

Three key ways artificial intelligence is changing what it means to compute.

still from Embodied Intelligence video
still from Embodied Intelligence video

These weird virtual creatures evolve their bodies to solve problems

They show how intelligence and body plans are closely linked—and could unlock AI for robots.

We reviewed three at-home covid tests. The results were mixed.

Over-the-counter coronavirus tests are finally available in the US. Some are more accurate and easier to use than others.

conceptual illustration showing various women's faces being scanned
conceptual illustration showing various women's faces being scanned

A horrifying new AI app swaps women into porn videos with a click

Deepfake researchers have long feared the day this would arrive.

Stay connected

Illustration by Rose WongIllustration 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 customer-service@technologyreview.com with a list of newsletters you’d like to receive.