As the oldest scientific academy in continuous existence, the Royal Society is a Fellowship of many of the world’s most eminent scientists. Up to 60 new Fellows (FRS) are elected each year in late April or early May, from a pool of around 700 nominations by existing Fellows.
“Science is, above all else, a human activity and I have had many inspiring collaborators throughout my career,” said Professor O’Hearn. “I’m particularly fortunate to have worked with both insightful theoreticians, like David Pym and John Reynolds, and great practical people, like Byron Cook and my colleagues at Facebook. I’d like to think that perhaps the FRS election reflects well on the work I’ve done together with these colleagues.”
Peter O’Hearn has made major contributions to the science and engineering of methods for ensuring program correctness. His impressive portfolio of research ranges from abstract topics such as mathematical models to the logics of programs, automated analysis of industrial software in the millions of lines of code and its application to industry.
Peter is known particularly for his work on Separation Logic in collaboration with John Reynolds. Building on previous work by Peter and David Pym, Professor of Information, Logic, and Security at UCL, on reasoning about resources, this fundamental theory opened up new possibilities for scaling logical reasoning.
“I have had the privilege to know Peter as a colleague and a friend for more than 20 years, said Professor Pym. ”His scientific insight and intellectual judgement have always been amongst the most impressive around. Peter has the rare ability to contribute both to fundamental science and to its effective translation into deployable, rigorously grounded, much needed tools.”
Peter then went on to develop Concurrent Separation Logic, which addresses the longstanding open problem of efficient reasoning about programs that operate concurrently. He received the 2016 Gödel Prize in recognition of this achievement.
Peter moved to Facebook in 2013 with the acquisition of a start-up he cofounded, Monoidics Ltd, while maintaining his position at UCL. The Infer program analyzer, developed by Peter’s team, has supported Facebook engineers to repair tens of thousands of bugs before they reach production. Infer is also used at Amazon, Spotify, Mozilla, and other companies.
“Peter is both a great theoretician AND a great practical influencer, said Byron Cook, Professor of Computer Science at UCL and Director at Amazon Web Services. “What makes Peter so rare is that he’s both at the same time: He has made profound inventions in the theoretical space, but more interestingly Peter has found application for these ideas in industry and then drove them all the way to products that provide critical value at several of the world’s largest IT companies (e.g. Amazon, Facebook, etc).”