Last author here, this is very much what I've worked on for most of my career. In this project, I had the idea of optimizing rendering instructions years ago, while I was writing https://browser.engineering/, but the hard part of this project was being very careful with the semantics of Skia itself. It's _super_ easy to write down rewrite rules that _seem_ correct, but are actually only correct when, say, something is opaque, or has the right blend mode, or two things don't overlap, or something like that. Which is why this paper focuses os much on carefully defining that semantics. We actually did the semantics in Lean because otherwise we couldn't consistently write correct rewrite rules.

Hey, I just wanted to say that this is, um, the fucking best.

I've been waiting for a literal decade for this, for the same reasons as the grand-parent poster. I literally had a chapter of my NSF CAREER proposal on this (failed, woof, but the reviewers were wrong! this rocks). The potential here is absurd. Eg, novel query optimizers and novel DB indexes could be created that, when connected to the right charting tools, would automatically emit efficient graphics and query results. Very, very cool work, thank you.