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.

As a former Skia contrib, this is cool as heck to read. It's exactly the sort of optimization work we had in mind when we wrote that SkRecord system, and I'm pleased that you were able to make use of nanobench. Back in those days we had just a few small optimizations that we could apply, mostly trying to eliminate unnecessary saveLayer() calls. Very cool to see it done in a modern way with Lean.

I've done something similar for DBus deserialization. It turns out that I stumbled upon something called fixed-point optimization for loops (in DBus: arrays), similar to what the JVM does according to Cliff Click's very interesting talks. It was pretty fun to write basically a toy optimizer that is even useful. As a friend said, it's probably overdesigned, but it was fun and it does yield code with not much left to improve. Well, except for embarrassingly optimizable types such as arrays of fixed-length elements.

We will probably see more such things as the consequences of the end of the free performance lunch play out. Hardware and software will specialize more, plenty of interesting work to do.

Hi folks! Last author here, happy to answer questions, very surprised to see this on HN. We had a blast working on this. Let me add that the Skia team at Google was super supportive, met with us many times to explain a lot of stuff.

I had the idea for this project years ago while writing Web Browser Engineering with Chris Harrelson (see https://browser.engineering/). Then a few years ago I made a first attempt at this project with Yuvaraj (https://droidkid.github.io/), but for various reasons we never got very far. I restarted the project with Bhargav (https://bhargavkk.com/) about a year ago, and focused much more seriously on the semantics of Skia itself, which made progress much more rapid. Still, I was, frankly, shocked by how good the results are.

You guys should take a look on Blend2D as well. Blend2D never hits the news, but it has been exploring similar topics for years. His work is so underappreciated.

This isn't my field, but if I'm understanding correctly this is so cool. I love the idea of being able to unlock optimisations by formally specifying behaviour.

On a side note I chuckled at the following -

> Web browsers, for example, struggle to render modern web pages

This is really interesting. I wonder how this might affect Chromes performance if they decide to implement such thing or just optimize the C++ code responsible for emitting sub optimal skia instructions

I wonder if same could be done to games. How much unnecessary work are modern games submitting to the GPU?

I do something related in my gpu library. After a few frames if the push constants don't change I compile the shaders in the background with them defined out by the preprocessor to reduce the size of the shader program (kind of like a branch predictor). I also store the entire pipeline in a graph data structure that I partition into segments that let me fuse and split kernels (though I hadn't implemented those optimizations yet). In my mind one issue with these GPU accelerated programs is that there isnt a runtime with the right level of information about the overall program to do compiler style optimizations, especially for complex programs.

(The library is called goldy, and until I spend some time on it the readme and docs are sadly LLM generated)

[flagged]