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

individual aging affects covid outcomes concept
individual aging affects covid outcomes concept

Anti-aging drugs are being tested as a way to treat covid

Drugs that rejuvenate our immune systems and make us biologically younger could help protect us from the disease’s worst effects.

close up of baby with a bottle
close up of baby with a bottle

The baby formula shortage has birthed a shady online marketplace

Desperate parents just want to feed their babies. They’re having to contend with misinformation, price gouging, and scams along the way.

"Olive Garden" NFTs concept
"Olive Garden" NFTs concept

I tried to buy an Olive Garden NFT. All I got was heartburn.

Our newest issue spells out what you need to know about the dizzying world of digital money.

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.