One of the fundamental aspects of research is choosing to work on problems or solutions before they are widely accepted as valuable, even just within a community of experts, let alone the public at large. I will share my thoughts on the challenges and satisfying aspects of working at a relatively uncommon intersection: doing systems research based on building prototype implementations over years, yet with a long time horizon where related implementations may not be ready for production for ten years or more. I will illustrate with a medium-granularity PLDI research area (verifying nontrivial code bases using proof assistants) and one of my particular experiences within it (verifying compilers for functional languages, leading up to the Fiat Cryptography project).

Started hacking on compilers & web-development tools in the late 1990s. Finished CS undergrad at Carnegie Mellon in 2003 and CS PhD at Berkeley in 2007, picking up mechanized proof of executable, decently practical systems with Coq as a main focus in between. Postdoc at Harvard through 2011, then faculty at MIT since. Author of Certified Programming with Dependent Types, a popular online & in-print introduction to using Coq at scale. Lately into building practical but clean-slate hardware-software stacks with end-to-end Coq proofs of everything digital, at the same time as developing a startup-company idea to trick ordinary people into using dependent types (with Ur/Web) to generate their business applications.