We noticed you're browsing in private or incognito mode.

To continue reading this article, please exit incognito mode or log in.

Not an Insider? Subscribe now for unlimited access to online articles.

  • Ariel Davis
  • Guaranteed Code

    Adam Chlipala is building a programming platform that could generate bug-free software.

    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.

    This story is part of the November/December 2017 Issue of the MIT News magazine
    See the rest of the issue

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

    Cut off? Read unlimited articles today.

    Become an Insider
    Already an Insider? Log in.
    Next in MIT News
    Want more award-winning journalism? Subscribe to Insider Online Only.
    • Insider Online Only {! insider.prices.online !}*

      {! insider.display.menuOptionsLabel !}

      Unlimited online access including articles and video, plus The Download with the top tech stories delivered daily to your inbox.

      See details+

      Unlimited online access including all articles, multimedia, and more

      The Download newsletter with top tech stories delivered daily to your inbox

    You've read of three free articles this month. for unlimited online access. You've read of three free articles this month. for unlimited online access. This is your last free article this month. for unlimited online access. You've read all your free articles this month. for unlimited online access. You've read of three free articles this month. for more, or for unlimited online access. for two more free articles, or for unlimited online access.