When You've Got EqSat, Everything Is a Compiler

Abstract:
We are surrounded by compilers in disguise. Whether optimizing circuits, planning database queries, designing machine-knit garments, automating proofs, or generalizing user demonstrations, these processes all rely on transforming program-like models.

In this talk, I will share my group's experiences across several domains where the compiler mindset has led to new techniques, tools, and cross-area connections. Over more than a decade, my students have followed this overarching research theme, eventually leading to the development of "egglog", a general equality saturation (EqSat) framework for building program verifiers, synthesizers, and optimizers, now applied across many fields.

Our key observation is that many hard problems can be reduced to term rewriting: repeatedly applying simple, local "find and replace" rules to transform programs one piece at a time. However, it is challenging to find just the right sequence of rule applications that works across all inputs, typically requiring delicate, domain-specific heuristics. In this talk we will see how egglog leverages both the e-graph data structure from congruence closure algorithms as well as Datalog and query optimization techniques from databases to enable robust, complex optimizations via simple rewrite rules.

Throughout the talk, we will explore how the "everything is a compiler" worldview helped us tackle a wide range of challenges and highlight how our collaborative, cross-domain approach has led to advances in floating-point accuracy, 3D CAD modeling, rewrite rule inference, and more.

Bio:
Zachary Tatlock is a Professor in the Paul G. Allen School of Computer Science & Engineering at the University of Washington and an Amazon Scholar at AWS. He helps lead the Programming Languages and Systems Engineering (PLSE) group at UW. He earned his PhD from UC San Diego. His research explores programming languages, compilers, and verification with applications to optimizing numerical accuracy, enabling computational fabrication, and improving hardware design tools. He is a recipient of an NSF Career Award, distinguished paper awards at POPL, PLDI, and OOPSLA, a UW FACET mentorship award, and research awards from Amazon, Google, and Meta. He can juggle and solve Rubik's cubes, but not at the same time.