The following exchange is part of an ongoing CS News series in which Cornell Computer Science faculty share some details about their research initiatives and teaching practice. For this session, we speak with newly arrived assistant professor Justin Hsu.
In 2017-18, Hsu was a postdoc in CS at Cornell, where he collaborated with Nate Foster, Dexter Kozen, and Bobby Kleinberg. He returns to Ithaca after serving as assistant professor in the Department of Computer Science at the University of Wisconsin, Madison. Funded by both an NSF CAREER award and a Facebook Research award, Hsu is launching several research projects and will begin teaching Fall 2021 with a graduate seminar on Probabilistic Programming.
JUSTIN HSU: At Work Formally Verifying Randomized Algorithms
CS News: Can you please describe some of your ongoing research projects and also share representative publications on these topics?
Justin Hsu: I design methods to formally verify that programs are correct, especially programs that use randomization. Such programs can be easy to show correct on paper, but surprisingly challenging for computers to analyze. In the past, I’ve developed methods to verify accuracy, incentive compatibility, Markov chain mixing, and various notions of algorithmic stability.
A particular focus of my work has been differential privacy, a rigorous definition of privacy that is currently under extensive study. I have investigated a variety of formal methods—such as type systems and program logics—to verify that programs are differentially private.
Can you tell us what you are most excited about in this research? And why?
There are two aspects that I find quite exciting. First, the programs we are aiming to verify have very different characteristics from the programs that formal verification usually targets—algorithms are usually small programs with highly complex proofs of correctness. The target properties are also more subtle, typically involving quantitative bounds measuring how good the algorithm is.
Second, a running theme in my work is to draw inspiration from how human experts analyze algorithms. While these arguments can appear highly technical, understanding the common patterns humans use to prove correctness can enable substantially simpler formal verification methods. I enjoy learning about novel algorithms from across computer science, and the ingenious arguments that experts use to prove their algorithms correct.
Please say something about what topics motivate your current teaching practice. For instance, how have your interests shaped your development of course content?
I've taught a few courses on verifying probabilistic programs, an area of PL and formal verification that has really taken off in the last few years. For instance, this summer I taught a short course called "Reasoning about Probabilistic Programs" at the Oregon Programming Languages Summer School. This fall at Cornell, I'm teaching a new graduate seminar called Foundations of Probabilistic Programming (CS 6182), where we are covering a new survey of the area that just came out last year.
At the undergraduate level, I've really enjoyed teaching courses that give students experience with functional programming, the kind of course that got me hooked on the field. I've taught this kind of course at Madison, and I'm looking forward to teaching the undergraduate functional programming course (CS 3110) at Cornell in the spring.
Looking ahead, can you articulate what you foresee as the long-term positive impact of your work?
In general, I am interested in analyzing algorithms from all areas of computer science. Correctness for these small, but intricate programs often relies on complex mathematical arguments, and bugs and errors can be very hard to find, even for experts. These algorithms play a crucial role in many of the most exciting areas of computer science today, and I hope methods that I develop will help ensure that these programs behave correctly.
Any remarks on returning to Cornell CS—what it means to be and what you’re looking forward to?
I had a great time during my brief postdoc at Cornell, and it feels great to be back after three years. Cornell CS has strengths in many areas of computer science, but especially those areas closest to my own work. I'm very happy to return to Ithaca, and I'm looking forward to building new collaborations.