Comment by eigenblake
13 hours ago
Wow! This is exciting. I have speculated that this would be possible. Since I've been learning about databases and dynamic db query optimization, it struck me as surprising that we didn't have similar things for more of our computational universe. Now that this is here, it makes me wonder what else we can optimize in using the same high level techniques.
The more you know about what you want to do ahead of time, the more optimally you can reorder your sequence of steps to give a better-than-naive solution. It makes me think about all software in terms of these abstract computation graphs and makes me wonder what else we can optimize automatically.
Of course, we do absolutely do need a formal model here, so we know what edits are possible, the same way db engines have relational algebra as their backing model. But this whole thing makes me feel like manual software optimization is soon to fall to AI. And I'm thinking that includes good-old-fashion AI first, not second, to LLM's. But I'm sure LLMs would be useful here too, especially for the formalization.
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.
I am a big fan of DB-style thinking, very much on the same wavelength as you :)
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.