This talk is about the unexpected learnings when a theoretical computer scientist was suddenly submerged into a fast-moving industrial software engineering practice.

I’ll recount the clash of cultures I encountered when, after 25 years in academia, I moved to Facebook with the acquisition of a program verification startup, Monoidics.

Traditionally calm and cool formal reasoning came in contact with a heated software development methodology based on rapid modification of large codebases (thousands of modifications per day on 10s MLOC). To my surprise, we found that static formal reasoning could survive and even thrive when we used techniques allowing it to adapt it to the company’s “hacker way” engineering culture, rather than the other way around. I’ll also describe how interactions with software engineers caused me to question some of the assumptions I brought from academic static analysis, and how I’ve come out the other side with new science spurred by that experience (most recently, incorrectness logic). Overall, I hope to convey that having theory and engineering playing off one another in a tight feedback loop is possible, even advantageous, when practicing static analysis in industry at present.

Peter O’Hearn is a Research Scientist at Facebook and a Professor at University College London. Peter has done research in the broad areas of programming languages and verification for over 25 years, having held academic positions at Syracuse University, Queen Mary University of London, and University College London, before joining Facebook in 2013 with the acquisition of the verification startup Monoidics. With John Reynolds Peter devised separation logic, a theory which opened up new practical possibilities for program proof, including the technology which led to the Infer program analyzer developed by Peter’s team at Facebook. Infer runs internally on Facebook’s code bases, detecting over 100,000 bugs which have been fixed by Facebook’s developers in the past five years. Infer is also used in production at number of other companies, including Amazon, Mozilla, Spotify and Marks and Spencer. Peter is a Fellow of the Royal Society, a Fellow of the Royal Academy of Engineering and he has received a number of awards for his work including the 2016 Godel Prize, the 2016 CAV Award and the 2011 and 2019 POPL MIP Awards. Peter received an honorary doctorate from Dalhousie University in 2018.