People of Programming Languages

An interview project in conjunction with POPL 2018  

 

JY: Let's start by having you tell us a little bit about yourself. What got you here?

BP: I fell completely in love with programming at age seven and for years spent all my spare time hacking on the University of Redlands' HP time-sharing system in BASIC. I wrote lots and lots of games, but at some point—I was maybe ten or eleven—I got interested in ELIZA and wrote a little ELIZA clone. Then I started trying to make variants on it. The pattern strings and the way responses were generated kept getting a little bit richer; I guess that was the first programming language I designed. It was super simple and domain specific, but it sparked a fascination that persisted.

So then how did I get to where I am now? Basically by staying on the same trajectory—except with lots of potential detours. When I was an undergraduate at Stanford, I was a linguistics major because there wasn't any computer science major at the time, and I thought linguistics was cool. And I was also deeply, deeply into music and vocal performance. So there was a period where I was really choosing whether I was going to be a computer scientist or a singer. I decided that, at least for me, it was better to have singing as a hobby and computer science as a career than the other way around, and I’ve been happy with the way that turned out. But it was a very hard choice at the time.

I finished at Stanford and went to CMU. I was still interested in linguistics, but the linguistics that they were doing at CMU at the time struck me as hacky; I wanted something more principled. First I tried software engineering: Nico Habermann was my advisor for the first year or two. I loved his sense of perspective and history—he was just a really wise man—but I didn't like software engineering that much because it was so difficult to judge whether your little academic solution to some issue afflicting gigantic software systems was a real solution or not. I have great respect for people who can function in that environment, develop good ideas, get good work done, but I found I wasn't one of them.

Programming languages research had an obvious historical resonance for me given my background in linguistics and playing with programming languages. It also had this property that you could tell when you had a right answer. It didn't tell you whether the question was interesting, of course, but at least you could know if you proved something. And I was lucky because this was a time when the PL group at CMU was really taking off. I worked with Peter Lee for a while, then ended up co-supervised by two of the greatest PL researchers, John Reynolds and Bob Harper.

JY: What are you most excited about these days, and is it surprising to you? Is it different from what you would've expected when you were doing your PhD?

BP: Jumping around between topics has been characteristic of my whole research career. But the common thread has always been some kind of connection both to real systems and to core PL themes. When I was doing my PhD and for a decade or so afterwards, it was all about object oriented programming and the theory of subtyping. Later on I got interested in file synchronization, which was not a PL-ish sort of thing, except I brought a PL-ish approach to it, trying to prove theorems to understand the essence of what a synchronizer should do and building software based on my understanding from those models. Later there was some crossover with databases that started with getting interested in bidirectional computation and the “view-update problem” and all that. More recently I got interested in security, and especially hardware based security. So it's different content from time to time, but what always say I like about my life is that I get to prove theorems on Mondays, Wednesdays, and Fridays, and hack code on Tuesdays and Thursdays, and it's all the same stuff.

What’s at the top of my priorities now is figuring out how to rigorously specifying, test, and verify real critical software. As everybody knows, this is an area that, has really exploded over the last ten or fifteen years, starting with things like CompCert and SeL4. A lot of people, including me, got the idea that “it’s time now”—the proof assistant technology is ready.

JY:. Something I wanted to ask about was how you choose domains. As you said, you've worked in a lot of domains. How do you decide what is the next one?

BP: In many cases it’s been scratching my own itch. In the case of file synchronization, I had my files on a laptop and a server and things kept getting out of date. I couldn't find a tool to do what I needed, so I started writing one, and then noticed I kept getting it wrong. So I got interested in specifying what such a tool should do. Also, with most of my projects, it’s been all about stumbling across great collaborators. In the case of file synchronization, it was getting together with Trevor Jim and Jérome Vouillon. With types for pi-calculus, it was Dave Turner and Davide Sangiorgi at the beginning. With OOP typing it was Dave Turner and then Martin Hofmann. With security, it was a combination of Steve Zdancewic softening me up and then later working closely with Greg Morrisett. And so on. I’ve been blessed with many fantastic collaborators.

JY: To you, what is a PL-ish contribution?

BP: PL people are good at taking complicated domains where people are creating new ways of doing things, but where it's too messy and not well understood, and pulling out the abstractions and the core concepts.

JY: I also wanted to talk about your many books. What got you started writing them, and how did they come about?

BP: The first book, Basic Category Theory for Computer Scientists, was totally an accident. CMU had a requirement that every PhD student do some kind of expository writing project. I was trying to learning about category theory at the time, and it seemed like a good project to try writing down what I was learning. So I wrote this paper, which turned out pretty well, so somebody said why don't you send it to Computing Surveys. Long story short, I got an acceptance letter with fantastically useful reviews, worked like crazy to incorporate them, and then at the last minute the head editor overturned the acceptance because he couldn’t understand it. Dave McQueen happened to be visiting CMU, and I was telling him this sad story. The next day he came back and said to me, "Call Bob Prior at MIT Press." I called Bob, reached him at home. I said “I wrote this tutorial on category theory,” and he said, "Yeah, I've seen it." I said, "I wonder if..." And he said, "Yeah sure." And a week later I had a contract.

The second book, Types and Programming Languages, was more calculated. Since I had already written a book as a PhD student, I knew how hard it was. I was under no illusions that writing any more books was a good idea. But at a certain point, a few years after my PhD, I started to feel like the field of programming languages, and especially the theoretical foundations of programming languages, was still lacking a really accessible book to pull it together. There were some beautiful books—Gunter, Mitchell, Winskel… But they were not that approachable for people without a strong math background. Although I understood that I was going to kick myself for getting into this again, I felt like there was an opportunity to write it all down in a comprehensive way that a field could coalesce around. So I took the challenge. It took me six years start to finish, probably averaging a third of my time. So two years full time.

JY: Was this pre-tenure?

BP: It was.

JY: And did you still have time for hacking during this?

BP: Some, but it definitely slowed me down. I realized at some point that as an academic you can do both hacking and writing, just not both at the same time! So you decide for a while I’m going to write a book. And the book is done and you say, okay now I'm going to build a system.

JY: What about the third book?

BP: Advanced Topics in Types of Programming Languages: that was the easy one. There was a lot of material that I’d have liked to put into TAPL, but either I was not the right person to do it or I ran out of energy before I got to it. So instead I convinced the right people for each topic to write chapters.

Then there’s the last book, Software Foundations. Actually, I should say “books” because it has recently undergone mitosis. There are three volumes now: two by me and my collaborators, and one by Andrew Appel, with more volumes to come. The original motivation was wondering whether a proof assistant could function sort of like a teaching assistant, to help students understand how to write correct proofs. And then the motivation for turning it into something like a book was a bit the same as with Types and Programming Languages: seeing an opportunity to bring a field together in one place and make it accessible. These proof assistants are getting amazingly capable now. We should be using them for teaching and we should be using them a lot more for our research, but it's hard to approach them. So it seemed useful to write an introductory textbook for a course that would get a lot of people up to speed.

JY: How do you train your students? What do you think is most important to teach someone about what programming languages research is?

BP: Here's one way of answering that. My most recent star student is Justin Hsu, who was co-advised by me, Aaron Roth, and Gilles Barthe. In the acknowledgments of his dissertation, he thanked Aaron for teaching him to think quickly and me for teaching him to think slowly. I thought this was great. One of the main things that I try to offer my students, or maybe just automatically offer because that's the way do research, is to really slow down and connect the dots—to make the argument crystal clear. And to continually connect the specific technical issue that we're stuck on right now to the overall context of what we're trying to do.

This gets back to the books as well. Probably the most important personality trait that has helped me succeed in writing for broad audiences is that I understand things pretty slowly. In lots of situations in research that's a liability, but it's a strength when you're trying to explain something because it's easier to remember what it was like to not understand and the steps that it took to get there.

JY: What's your favorite thing about your POPL community?

BP: One perfect example of what’s great about this community is the reviews we write about each other's papers. I've published in lots of other areas, and the standard of reviewing in POPL and related conferences is not just a little bit better: it's a whole different animal! The kind of care and generosity that people expend on on other people's work, trying to understand it deeply, acknowledging what’s good while holding each other to a high standard of intellectual rigor. We have a community that values rigor, creativity, and friendliness. That’s just a killer combination.

JY: Anything else you’re thinking about?

BP: I’ll just mention one more: climate change. It’s not a natural topic for a PL person, and not easy to contribute to technically, but it’s something I’ve been trying hard to wrap my head around because I have two young kids and I want to leave them a world they can live in. We computer scientists burn a shocking amount of fossil fuel getting to conferences, so there’s an extra sense of responsibility. I’ve been doing a lot of reading, discussing, and writing about what steps we might take, as a community, to move things in a better direction.