Nathaniel Yazdani

Education

• BS in Computer Science, University of Washington, Seattle

Biography

About Me:

• Hometown:  Brush Prairie, Washington
• Field of Study:  Computer Science
• PhD Advisor:  Amal Ahmed

What are the specifics of your graduate education (thus far)?

So far, I have jumped onboard the Oxide project with Amal Ahmed, my advisor, and Aaron Weiss, a fellow PhD student. My role has been to mechanize the theoretical developments --- syntax, semantics, and metatheory of the Rust programming language --- using the Coq proof assistant. The work leverages my prior subject experience and skillset, and the expansion to the research effort dovetails nicely with the Oxide project's overarching goal: an approachable, extensible theory of Rust to serve as the elemental prototype for derivative work in the research community.

Outside research, I am also taking an engaging course on program analysis (CS 7580 Intensive Construction of Software and its Engineering) from Jan Vitek, another professor in NU PRL.

What are your research interests in a bit more detail? Is your current academic/research path what you always had in mind for yourself, or has it evolved somewhat? If so, how/why?

Ultimately, my research interests are about easing the construction of correct software, especially with respect to a known specification. I focus particularly on approaches based in formal logic and automated reasoning; in other words, my research emphasizes an interplay with formal methods. In line with that, I am excited by the development of theory that is mathematically insightful yet practically applicable, as such results in theory offer an opportunity in practice to utilize formal methods more effectively, thus reaching problems of greater scale and complexity.

Throughout my undergraduate and master's studies, I knew fairly confidently that I wanted to pursue a research career, and my exact research interests (always within programming languages and formal methods) were gradually refined during those years. That self-understanding enabled me to choose an advisor and institution well matched to my research path, which has been great so far.

What’s one problem you’d like to solve with your research/work?

In a (potential) future project, I might address the lack of interoperability among proof assistants (i.e., programming languages with some special design qualities), particularly the three major ones (Agda, Coq, and Lean) with the most closely related theory. Interoperability among these proof assistants would allow users of each to share in the value of the others' various proof libraries, which were originally engineered over many person-decades.

Since my colleagues in the SILC group have done prior research on safe language interoperability, this research effort could build on those results, extending to the more complex theory for a proof assistant, and then implement the developed theoretical ideas into the actual proof assistants.

What aspect of what you do is most interesting/fascinating to you? What aspects of your research (findings, angles, problems you’re solving) might surprise others?

When an especially thorny challenge emerges in a research project, I really enjoy the creative process needed to figure out a solution. In particular, searching through the literature for applicable ideas/results reveals an amazing diversity of knowledge and perspective; even if not immediately significant, the broader context gained often leads to better solutions and even new research directions down the road.

Those outside my area might be surprised that most such research relies critically on algorithmic tasks either undecidable or computationally intractable (i.e., NP-complete or worse). Despite that, decades of research has yielded algorithmic techniques that routinely solve complex instances of such tasks at seemingly infeasible scale; the trick is that these performant algorithms are not fully general but are instead specialized to "real-world" instances. For example, a modern SAT solver easily scales to million-variable formulae constructed by client applications, yet that same solver inevitably spins out on randomly assembled formulae with only thousands (or merely hundreds) of variables.

What are your research/career goals, going forward?

Long term, I hope to join the faculty of a research university, so that I may continue my research endeavors while also teaching and mentoring the next generation of students.

Where did you grow up/spend the most defining years of your childhood/young adulthood?

I grew up in the rural outskirts of Portland, Oregon; there was literally a dairy farm down the street from me! As an adolescent, I spent more time in the metro proper, attending community college and interning at a tech company. As much as I miss the countryside scenery, living in the city has been much more fun.

Where did you study for your undergraduate degree? Any reason in particular behind your choice (a program you were excited about, a city you love, a researcher you wanted to work with)?

My undergraduate and master's studies were done at the University of Washington (UW) in Seattle. I chose UW for the strength of its computer science program and, admittedly in part, for its location in Seattle, keeping me in the great state of Washington. While at UW, I was fortunate to make many friends and collaborators out of the students and faculty in Programming Languages & Software Engineering (https://uwplse.org). I owe a lot of my intellectual development to the computer science program's strong culture of supporting and encouraging undergraduate participation in research.

Recent Publications