Formal reasoning and the hacker way (keynote)

In 2013 I moved from to industry after over 25 years in academia, when Facebook acquired a verification startup, Monoidics, that I was involved with. In this talk I’ll recount the clash of cultures I encountered, where traditionally calm and cool formal reasoning techniques came in contact with a heated software development methodology based on rapid modification of large codebases (thousands of modifications per day on 10s MLOC). I will tell how we found that static formal reasoning could thrive, if certain technical approaches (based on compositionality), how the industrial experience caused me to question some of the assumptions I learned in 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 science and engineering playing off one another in a tight feedback loop is possible, even advantageous, when practicing static analysis in industry at present.