remywang

Sigh, I recently got into stereo photography and saw there's a shortage of transparency film. I suppose the stock's not coming back up any time soon. We can't even take photos thanks to the clankers can we.

I added the quote after seeing the parent comment-thanks for the feedback.

I agree there is a spectrum, but we at least have to be honest with ourselves: are we really sure AI generated code is following the spec? On the other hand, with progress in proof automation, it is now feasible to formally verify AI generated code, and that allows us to specify program behavior formally, and a formal specification is again a program in itself.

Then don't grade the homework! I have in-person quizzes in my class, and the students are motivated to do the homework anyways because it prepares them for the quiz.

So I spent some time poking at the released 0.4-beta code. Controversy aside, it is interesting to see an open source system that beats ClickHouse on ClickBench - 4 out of the 5 systems ahead of CH (Umbra, elosdb, Hyper, CedarDB) are all closed-source, while the only open one is pivotlake.

What makes pgrust fast? There's no one single reason, but a combination of techniques like dictionary encoding [1], zone maps [2], late materialization [3], vectorization [4], and a gazillion others. It's not unlike all the countless optimization passes in a compiler.

None of the optimizations are groundbreaking - in fact, I could find a counterpart of every optimization I checked in ClickHouse as well! So why is CH still slower?

I believe the difference is in when they decide to apply each optimization. Unlike compiler optimizations which are usually beneficial, DB optimizations are highly data-dependent, and the query planner needs to turn them on an off based on data statistics. For example, CH is more conservative in applying dictionary encoding, and it basically doesn't get used at all for ClickBench.

Turning off dictionary-related optimizations in pgrust immediately made it 5x slower (from 3.8s to 20.4s on my machine), while ClickHouse takes a total of 15.0s.

This points to one important nuance in benchmarking - when all you target is one single benchmark, you can be more aggressive during query planning, as plans that work well for one query probably also work well for others, due to characteristics shared among queries/datasets. But when you build a system that needs to support millions of users, you have to be conservative with optimizations.

[1]: https://motherduck.com/glossary/dictionary-encoding/

[2]: https://motherduck.com/glossary/zone-map/

[3]: https://arrow.apache.org/blog/2025/12/11/parquet-late-materi...

[4]: https://clickhouse.com/resources/engineering/vectorized-quer...

To turn off dictionary-related optimizations in pgrust, I used the following setting:

  SET pgrust.gravity_road_off = 'dict.entries,percode.table,percode.length,verdict.coderange,
    code.carry,code.render,code.front_part,code.front_dense,code.front_light,code.sparse,
    code.cut,code.heads,key.codeif,prefetch.fp,text.frame';

Thanks for the explanation, can you release the source of 0.4-preview so that people can understand what was going on?

Hang in there! What you can build knowing how to code is drastically different from what promptards can build. Imagine trying to build a car without knowing anything about car building - you’d just get the most generic boring clunker anyone can design.

Every verification needs a spec, and in this case the spec is the Postgres implementation. I think we can and should do a lot better than taking 2.6 million lines of C code as the spec.

In general, the spec must be human readable, and I believe to achieve that we must do away with SQL. Putting aside the thousands of pages of SQL standard, even the core subset has a gnarly semantics due to issues like nulls.

A simpler semantics is one of the main motivations behind Prela [1], and despite its simplicity, we now know it’s powerful enough to express thousands of queries in the wild [2], as well as run doom [3].

[1]: https://prela-lang.org/

[2]: https://github.com/remysucre/prela/tree/sqlstorm

[3]: https://github.com/remysucre/prela/tree/doom/

> I wrote a compiler that can translate both Rust and C code into Lean

How do you verify this compiler is correct? To do that, I think you at least need a formal semantics for both C and Rust in Lean, both sound like Herculean efforts

Services you were responsible for

Do not

> Eight projects, including … SQLite … show no grant or sponsorship in any public funding source the analysis checked

SQLite has a list of sponsors right on the homepage https://www.sqlite.org/

So much nonsense on HN front page these days, the algorithm desperately needs to be redone

I greatly enjoyed reading their sail log crossing the Pacific Ocean, very poignant and down to earth: https://100r.co/site/busy_doing_nothing.html

Yes that’s the idea, these conjectures basically say “there’s no better algorithm than the naive/brute force one”. It’s like if P!=NP, then there’s no (asymptotically) better algorithm for SAT than naive backtracking search.

3SUM is (was?) one of the key conjectures in fine-grained complexity, mostly used to derive lower bounds for other problems. As such, most did not think a subquadratic algorithm was possible. Similar for APSP

What does this add over https://dblp.org/?

By the same reasoning, why should I care about the output of someone else’s clanker if I can just get it from my own clanker?

But to answer your question, I do still care about software being maintained by someone who can make design decisions instead of just yielding control to bots who tend to produce mediocre designs.

One cool factoid about PEGs is that it is an open problem if they can parse all context free languages.

lol along those lines yes

This can be good advice if worded a different way: only go to grad school if you really love doing research. If you love research, then the right graduate program is the best place for that. Getting a PhD was the hardest thing I’ve ever done but I don’t regret a single day of it.

Explainer videos should focus on explaining, but these videos are nearly content-free.

Kurzgesagt makes some of the best explainer videos, and they spend most of their time writing the script, not making the animation: https://youtu.be/uFk0mgljtns?si=NCMxIYGUYY-BbQgB&t=75

I’m so confused, how are you supposed to perform aggregation without reduce? This is like saying “I like plus and times, but I don’t like divide because it’s hard.” I mean sure, but you need it??

Very practical approach to “query optimizer as a service”, but I find it cursed that we have decided SQL is the IR for databases

What website are you talking about? This has nothing to do with AI.

The root of all these is the culture in mathematics (and science in general) to only reward those who “get there first”. This creates a perverse incentive to compete. When no one can out compete a tireless swarm of AI, no one gets rewarded any more.

But nothing’s stopping anyone to still work out an alternative proof, or a more elegant proof, or just trying to prove for the sake of understanding, just like doing homework without looking at the solution. It’s just that you can’t get paid doing that anymore.

People saying “he should have opted out” are missing the point. OpenAI can and should check their training data for leakage in the face of big breakthroughs like these. It’s the burden of the author to appropriately cite their sources.

It’s like a scientist refusing to give another one credit and say “sucks to be you, you shouldn’t have shared your idea with me”.

Light is making a flip phone [1], and it's somewhat hackable now that they release an SDK [2]

[1]: https://www.thelightphone.com/shop/products/light-flip

[2]: https://developers.thelightphone.com

There has been no movement on this since 2023, and Migicovsky is now busy with reviving pebble

It's rather convenient for OpenAI that user logs are de-identified before being fed into training, so they can say "there's no way for us to check if we plagiarized our user's work, because user data is private".

It's also difficult to imagine any competent AI researcher would overlook the possibility of training data leaking into the test, especially given that they know the users have been using their model to work on the same problem, and that they jumped on the problem after hearing rumors of the breakthrough.