I’m a computer-science professor at MIT and cofounder of Nectry.

My blog Structure and Guarantees considers how to build AI systems that we can actually understand and trust. The usual academic stuff is on my home page.

I work broadly on creating better abstractions for programming. The most-persistent theme of my work is formal methods, with proofs about programs that are credible with minimal trust requirements. We would rather not trust computer processors, compilers, operating systems, databases, cryptography, programming-language designs, individual applications, or theorem-provers themselves—and parts of my research have addressed removing trust in all of the above, including in integrated systems with proofs that cross such layers.