With (virtual) ICFP 2020 just around the corner, it’s a great time to get to know a few people in the programming languages research community, especially since we aren’t meeting each other in person this year. People of PL is a series of interviews that continues in the same vein as the People of POPL and the People of Language Design and Implementation interviews that were done by Jean Yang, Brandon Lucia, and Minjia Zhang.

In this edition, John Wickerson meets Derek Dreyer, who is a tenured member of the Faculty at the Max Planck Institute for Software Systems in Saarbrücken.

J: Tell me about the journey you took to get to your current position.

D: Well, I did my undergraduate at New York University. I didn’t even know that “programming languages” was really a field of study until I took a course where I learned about Scheme, ML, and a little Haskell. I thought they were fascinating, and I decided to go to grad school at Carnegie Mellon University because of that. My PhD there was with Bob Harper and Karl Crary, and it took a while – about seven and a half years actually. I think my thesis work was interesting, but not earth-shattering.

J: It was on module systems, wasn’t it?

D: Modules, yeah. And then I did a postdoc at the Toyota Technological Institute at Chicago, which was a pretty nice place to be, though I was basically just continuing with my own work and didn’t really collaborate much with anybody, except a little bit with Matthias Blume. Then I was very fortunate to get the job at MPI – the institute had only been founded a couple of years earlier, and they were just starting to hire. I joined in 2008 as only the third Faculty member, and I’ve been there ever since.

J: How does working at a research institute compare to working in a University?

D: Well, the biggest thing is that I have a lot more time to do research. Most people at the normal academic institutions have to write grants all the time, and teach too, and I just don’t have to do either of those things nearly as much. I’m totally amazed by other academics – how they find the time to do all that and have a personal life too.

The one big grant proposal I did write was RustBelt, which was funded by the European Research Council (ERC). Actually, that’s not quite true: I wrote another ERC proposal back in 2011 or so, but that was not successful. It was actually a very bad proposal – it was too early, and I didn’t really know what I wanted to do.

I would say that having the freedom not to worry about writing grants and so on was very important for me. The thing is, when I started at MPI, I really didn’t know what I wanted to do – I just had some ideas. I think that if I had had to worry about grant-writing and teaching, then I would not have been able to spend so much time really developing those early ideas, which have had a lot of influence on the stuff we’ve done ever since.

J: Would you enjoy doing some more teaching?

D: I am actually doing some teaching right now. I’ve been a professor for the last couple of years at the Saarland University, where I have a very light teaching load. There are a few topics that some collaborators and I would like to develop pedagogical material for, such as using the Iris framework in Coq. We’ve had several meetings about doing this, but it’s hard to get it off the ground because it’s nobody’s actual day job. It gives me enormous respect for people like Benjamin Pierce, who has somehow managed to produce multiple textbooks and still publish like crazy!

J: What is the problem that drives your group’s research at the moment?

D: We’re working on a number of different things to do with building firm, reliable, formal foundations for real programming languages. Of course, we’re not the only group doing that, by any means; for instance, I find the work of Peter Sewell’s group in Cambridge very inspirational. I like to think of what we do as looking at real languages in their somewhat exciting and somewhat ugly reality, and then trying to build foundations for them. Partly we want to understand what’s going on, and partly we want to help the development of those languages.

More concretely, we’ve done a lot of work at the intersection of several topics that have often been studied independently, such as type systems, relaxed memory concurrency, and interactive theorem proving. We use Coq a lot, and we use separation logic as a key tool for tying things together and for modular reasoning about program state. All of these things have come together in the RustBelt project over the last four or five years.

J: Could you say a bit about this RustBelt project of yours?

D: Well the original goal of the RustBelt project was very simple: it was to build the first formal foundations for the Rust language. One of the things that makes Rust really interesting is the interaction between two features. On the one hand, it has an expressive type system for controlling mutable state, and on the other hand, it really embraces the use of unsafe code for extending the power of this type system. I was very excited when I first heard about Rust. I thought: oh, this is just the kind of thing we’ve been building foundations for for the past ten years, just because I thought it was interesting. And then it turned out that they were actually building a language like this!

Anyway, we’ve been building a formal explanation of how this all works, and in some cases finding a few bugs, but mostly not. In fact, I’ve been pretty impressed by how few bugs we’ve found – the whole thing has been very well put together.

J: What’s your favourite part of your job?

D: Working with students.

J: Aw, that’s exactly what Alexandra said. Pick something else!

D: Oh, she said the same thing? I mean, I was a bit torn between “working with students” and “writing papers”, because I really like writing papers. But then, I’d rather work with students and not write papers than I would write papers and not work with students.

J: What is it that you like about working with students?

D: It’s because they know much more than I do, which is great! I find that I can start working with a student, and in the beginning I have a little edge and I can teach them something. And then at some point they take over and they start charging in some new interesting direction, and just surprising me all the time! And they’re such fun to work with. They enhance the scientific aspect of the job tremendously. I would never have gotten anywhere without having such great students, and postdocs as well.

J: What are your top tips for getting good students?

D: Hm, I don’t know. I still haven’t figured out a reliable algorithm for that. One thing is that I’m very picky – I only take on students who I personally get along with. People who I look forward to having meetings with.

J: So you must have interacted quite a bit with each of your students before taking them on?

D: Exactly. I’ve been very lucky in that for the most part I’ve been able to actually work with a lot of students, either in an internship or in some sort of short-term project, before I took them on. It’s very difficult to know what it will be like working with a student until I can at least do some kind of project with them.

J: Is your main criterion finding somebody who you can get along with?

D: Well that’s one thing, but another thing is their technical strength – how quickly they can pick up ideas. And how enthusiastic they are. Of course, these things are hard to gauge – for instance, a student might be very enthusiastic about one thing and not about another. There’s no silver bullet. All I can say is that I’ve been very fortunate to work with a number of fantastic students and postdocs. And that’s the biggest source of any success that I know.

J: And what’s your least favourite part of your job?

D: Hm, some students asked me this at lunch, and I didn’t know the answer then either! I have a pretty great job, to be honest. Ok, I’ll say something relatively obvious: I don’t like acrimonious debates among the faculty about anything. They happen once in a while, and I don’t like that. But this is a small thing, really. Ultimately, it’s a great job.

J: You mentioned that you enjoy writing papers, and you’ve been rather successful at this, particularly this year, with four papers at POPL 2020. What’s your trick?

D: I try to write papers that I’d want to read. And I do make every effort to read carefully the final version of each paper, though it’s sometimes hard to find the time to do that before the deadline! I try to make the whole paper understandable. I focus on not just writing the paper for the experts, but on making the most important parts of the paper accessible even to non-experts.

When I first started at MPI I was writing a large part of each paper, but nowadays I’m trying to help my students more by writing less. Nowadays I might draft the introduction, and sometimes not even that. I really try to get the students to write as much as possible, and then I give feedback, and then we iterate. This takes a lot of time, of course, but it’s the only way to learn. It’s the same with giving talks.

J: Yes I think the talks that come from your research group do tend to be rather high quality, and often quite accessible.

D: Well, when I read other people’s papers, or when I go to other people’s talks, much of the time I have no idea what’s going on…

J: Me too!

D: …even in topics I’m supposed to be an expert in! So I try to prepare talks that I would want to listen to.

J: Now, you’ve been to quite a few SIGPLAN conferences over the years?

D: My first conference where I had a paper was POPL 2003, which (as with POPL 2020) was also in New Orleans.

J: Right. So, how would you say the field has changed over that time?

D: I think the field has gotten more exciting. There’s a lot more really interesting work on formal methods, and on the combination of formal methods with programming languages. I feel like people have moved into proving a lot deeper and more interesting properties, scaling up to more complex languages, and reasoning about big systems. And the systems people are taking notice of this – just in the last couple of years there has been a really serious interest in formal verification from the systems community, and that’s very exciting.

J: Which computer scientist would you most like to bring back to life and have dinner with?

D: I guess an obvious person I’d love to talk to is John Reynolds. The thing is, I did my PhD at Carnegie Mellon University, but I barely ever talked to him. I was not very proactive about learning new things when I was a grad student – I guess I sort of had my head in the sand a lot of the time. John was developing separation logic at the same time as I was there, and I even remember listening to various talks about it. I didn’t really get it – it didn’t seem that exciting to me. But now, of course, I’m spending a huge part of my career working with separation logic. I do remember talking with him about some work I’d done on relational reasoning – he said to me “I’m glad I got out of this business before things got so complicated!” I guess that if we had dinner together, I would hope to convince him that we’ve simplified and consolidated things quite a bit with our work on the Iris verification framework.

J: How do you spend your time when you’re not working?

D: Well, I spend a lot of time with my family: my wife Rose and 5-year-old daughter Alma. We love to play games. Alma is incredibly good at Set, and lately she’s also gotten into geography games, so I’m learning more than I ever wanted to know about flags, populations, highest altitudes, neighbouring countries. It’s very difficult to compete with a child’s brain when it comes to storing that kind of information, but it’s a lot of fun.

In my remaining free time, I of course indulge in social media and movies and TV like everyone else, but I also listen to music a lot, mostly classical and jazz. The last couple years, I’ve been trying to really come to grips with specific pieces that were written by composers I love but that were not so accessible to me at first. For example, I spent a long time last year learning to like Britten’s Third Cello Suite, which initially I found mystifying, but after listening to a dozen recordings many times, it became one of my favourite pieces of his. Right now, I’m working on Shostakovich’s Fourth Symphony, which is more difficult because it’s borderline incoherent, but I’m getting there. The Neeme Järvi recording is spectacular.

J: And I know you’re also a big fan of whisky.

D: Heh, yeah, I do spend an embarrassing amount of time drinking Scotch whisky and reading whisky blogs like whiskyfun.com. I have over 150 open bottles, which is crazy but it’s pretty much the only drink where you can have a “liquid library” like that and the liquid stays in pretty good condition for years and years. I can also say from experience, well, I probably shouldn’t say this, but drinking really good whisky can sometimes help me over writer’s block when I’m trying to draft the introduction to a paper. My tendency is to be a bleeder rather than a gusher, meaning that I naturally write very slowly and constantly edit my text as I write it, it’s hard for me to just pump it out. And for introductions, this can be a problem because it often takes so many iterations to figure out the right line of thought. So whisky is very helpful because on the one hand I find it inspiring, and on the other hand it loosens my inhibitions, so I can gush more. It has led to some of my more spirited introductions, if you’ll pardon the pun, but don’t ask me to which papers – I can’t remember!

J: So, what would you be if you were not a computer scientist? A conductor? A whisky sommelier?

D: In my fantasy world, I would be a filmmaker or screenwriter, something creative like that. Like I said before, the part of my job that I love the most aside from working with students is writing papers. I really like taking complex technical work and extracting the key insights that can make the work more accessible to others. So I often wonder if I could somehow apply my writing talents to creating something more artistic yet still accessible.

The closest I’ve come is my recently neglected Herr Dreyer blog, where I’ve ventured into more creative writing territory, although I’m not sure I would call it “artistic” exactly. I wrote one post called On Science As Art, where I talked about how I view my current career as a reasonable substitute for being a “real artist”. You might remember that post, John, since it holds up your Ribbon Proofs paper as a rare example of artistic PL research!

J: Yes, I remember being delighted by your kind words. But I think people reading this will assume I just edited in some self-promotion at this point in the transcript; they won’t think you actually said that.

D: Said what?

J: Never mind. Anyway, talking of your blog, I do remember particularly enjoying one of your posts from several years ago about your struggles with “imposter syndrome”. Do you have any plans to write more on that theme?

D: Yeah, I do. It’s funny, a lot of people have told me how much that post meant to them, but I didn’t actually intend it to be meaningful! I was just trying to think of interesting stories to tell, and I thought, oh I’ll write some history about my papers, starting from the beginning. And regarding my first paper, I thought it would be interesting to share how much trouble I had getting started in research and how I almost got kicked out of grad school. And then somehow as I was writing the post, this stuff about imposter syndrome just tumbled out and was kind of raw and emotional. I mean, I knew I was describing a formative moment in my life, but I’m not sure I realised until I wrote the post just how traumatic it was. Even now, I still get these intense episodes of imposter syndrome on a regular basis, and I think they stem from that feeling of worthlessness that I first recall experiencing in grad school. Over the past few years, I’ve been learning ways to cope with it, but it remains a constant struggle. I hope to find more time to write about it!

J: Ok, here’s my last question: what is your favourite programming language, and how much actual programming do you do nowadays?

D: Well, I’m more of a theoretician, as many practitioners would gladly tell you, so I don’t actually program very much at all. It’s mainly my students who do a lot of programming, and most of that is in Coq, which we use in almost all of our papers now. As for my favourite language, I’m not really sure. I guess the reason I got into this business was because of Standard ML and Scheme. I found those two languages very inspirational. I’ll say Standard ML is my favourite – that’s the language I’ve actually done the most programming in. I think it was a very beautiful language in many ways – it’s kind of sad that it’s not being developed any more.

J: Thank you very much!

D: Sure, thank you.

Disclaimer: These posts are written by individual contributors to share their thoughts on the SIGPLAN blog for the benefit of the community. Any views or opinions represented in this blog are personal, belong solely to the blog author and do not represent those of ACM SIGPLAN or its parent organization, ACM.