Very broadly, I want to make it easier for the average programmer to write correct code. This can be achieved through a variety of avenues, and a lot of them interest me! Most of my explorations so far have been through the use of interactive verification tools: can they be made more efficient, powerful, and intuitive? I'm interested in continuing work in this space, but also branching out to solve more theoretical problems: how can we develop better type theories, stronger categorical foundations, for dependently typed proof assistants? Can we employ optimizations without making arbitrary decisions, and rather approach such problems systematically, through generalized frameworks?

The world if we all verified critical sections of our software...