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, first author here, and you are right to think that there are a lot of computational processes that can be "cast" into tiny programming languages. This is more apparent with DB queries (and I think there is a long list of papers on this topic) but less for graphics, which is why I found this so exciting to work on. If you peek at the last paragraph in the related works section of the paper, you will see a list of papers that try to do exactly that for a variety of graphics/fabrication domains.

I think good-old fashioned AI is the key here! Lot of the Lean proofs are discharged by a proof-search procedure called "grind". And if "grind" fails, an LLM can read the logs of the failed proof-search and figure out if there are any missing theorems needed.