David Holland

Software is terrible. These days this is a universal truth that permeates everything. What can be done about it? Years ago I got involved in operating systems development because you can’t build on sand. Later on I got into languages and tools, and also teaching, because empowering others vastly increases one’s reach and ability to mitigate the general catastrophe. Nowadays my top research interests tend towards formal verification, because it’s now reaching the point of being practical for deployment. However, I’ve been a lot of places and some of them have stuck in their own right, so the full set of my research interests range from concurrent programming models to kernel internal architecture to query languages for graph-structured data and a lot of stuff in between.

Background

David worked for many years in Margo Seltzer’s lab at Harvard and, after finally writing a dissertation on program synthesis, joined Galois in 2022. He also wrote the OS/161 instructional operating system, and in his remaining spare time is a NetBSD committer, where his primary concern is cleaning up code horrors that arise from non-local structural and design problems.