Adam Chlipala joined the MIT faculty in 2011, after finishing his BS in computer science at Carnegie Mellon in 2003, PhD in computer science at UC Berkeley in 2007, and postdoc at Harvard. He works on designing and implementing new tools and infrastructure to support applications of computers. Most projects use the Coq proof assistant to establish correctness of systems, and one of his main obsessions is how to apply scripted proof automation and other techniques to promote readability and maintainability of large certified systems, spanning the abstraction gap from hardware designs to low-level programs like operating-system kernels to high-level application logic as with clients of relational databases. He also works in the design and implementation of functional programming languages, as in the example of his domain-specific programming language Ur/Web, which brings strong mathematical guarantees to the world of Web applications.