remywang

Joined 6 years ago

Karma

894

Submissions

143

Member since

Oct 3

https://remy.wang

View on Hacker News

Recent submissions

Comment · 5 days ago

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.

Comment · 7 days ago

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';

Comment · 8 days ago

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

Comment · 8 days ago

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.

Comment · 8 days ago

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/

Comment · 8 days ago

> 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