malisper

To give you a sense of how fast it is, pgrust on a c6a.2xl is faster than ClickHouse running on a c6a.metal, a machine with 24x as many cores and costs 24x as much.

Edit: And now it's been accepted: https://benchmark.clickhouse.com/

[0] https://github.com/ClickHouse/ClickBench/commit/56535d29e825...

[1] https://github.com/ClickHouse/ClickBench/commit/89cc76e1e4e2...

Comment · 6 days ago

The preliminary ClickBench results for -beta are in[0]. The geomean across all runs came out as 7% faster than -preview[1]

[0] https://github.com/ClickHouse/ClickBench/commit/56535d29e825...

[1] https://github.com/ClickHouse/ClickBench/commit/89cc76e1e4e2...

Comment · 6 days ago

If you don't trust the logging, here's a script you can run that instruments the binary and shows that the files called out for cheating don't run during the benchmark: https://pgrust.com/downloads/archive/2026-09-clickbench-snap...

It instruments the files that were called out in the PR, then runs ClickBench. You can run it and see that the code in those files doesn't run.

If you can find anything suspicious in the binary, let me know, and I'm happy to dig in

Comment · 6 days ago

> I've seen his explanation. I don't find it convincing, at all

You don't have to take my word for it. If you want you can inspect the binary yourself: https://pgrust.com/downloads/archive/2026-09-clickbench-snap...

You can run the binary with PGRUST_GRAVITY_REPORT=1 which logs the code path hit for every query. You'll see that all the code goes through the general query path. We did have hand-rolled code in the binary, but we used it for testing. The code is not used when running the benchmark. We also did not use a results cache. Warm runs still scan all the data. You can verify all of this

You are right, though, that it did support a narrow set of SQL. It supported scans, group bys, sorts, and filters. That's enough to run all the queries on ClickBench, but failed on functionality not tested by the benchmark like subqueries

Comment · 6 days ago

Unfortunately, we have some sensitive stuff in our internal repo that we can't share. Fortunately, you can check the binary we submitted yourself: https://pgrust.com/downloads/archive/2026-09-clickbench-snap...

You can run it with PGRUST_GRAVITY_REPORT=1 and it will log the codepath that was hit for every query

On the lint, yes, I'm aware. It's one layer of defense. When we were prepping for the 0.4-beta release, we generated a large number of fresh queries and made sure the engine runs them and performs well across all of them

Comment · 6 days ago

Fair point: the 0.4-beta source doesn't prove anything about the benchmarked binary. So don't take my word for it or rely on the source we published as evidence. Instead, check the submitted binary itself: https://pgrust.com/downloads/archive/2026-09-clickbench-snap...

If you run it with PGRUST_GRAVITY_REPORT=1 it will report the code path hit for each query. You can see that all the queries go through the general query engine

The binary does contain hand-written kernels in the irprobe files. These were used for testing. You can validate that when running the benchmark, those files are dead code

The engine supports a narrow subset of SQL: scans, group-bys, filters, and sorting. That's enough to run ClickBench. It doesn't support e.g. subqueries which is why some of the follow up queries failed

Comment · 6 days ago

> This aged like milk. pgrust was caught cheating on all benchmarks this week.

Can you back this up? Our code is open source here[0]. You're free to audit it and benchmark it as much as you want. You'll find it's just as fast as we claim it is

[0] https://github.com/malisper/pgrust

Comment · 6 days ago

My goal isn't to "prove" the software is correct. My goal is to find as many bugs as I can with the least effort. If I'm able to find all differences in behavior between pgrust and Postgres, sans bugs in the compiler, that's a real win for me

fwiw, I wouldn't say working at the assembly level solves the problem. You now need to make sure that your definition of the assembly behavior is correct

Comment · 6 days ago

Happy to chat about it. I looked at Aeneas, but as described, it only supports safe Rust. I also need C support so I can prove both the C and Rust code

Right now, I wrote a compiler that takes C and Rust code and compiles it to Lean. Then I have an LLM write a proof that the C and Rust code behave identically. I've been able to prove equivalent behavior for about ~70k lines of C code with pgrust.

The issue I've started to encounter is that the context needed for each incremental proof has kept growing, and things have slowed down dramatically. My hunch is that the speed is the time it takes to prove a line of code is on the order of O(n^2) of how much you've proved so far

I'm looking to see if there are ways to shard things so the required context scales better. Today I was going through the formal verification work Anthropic and Theorem published a few days ago, and it looks like they used some sort of orchestrator to manage all their proofs and ensure good clustering of similar code. I'm seeing if I can get an approach like that to work

It's just difficult enough that I think it's doable if done right. Half of me is debating if I should wait until the next model release because any improvement in model performance will help a ton

Comment · 6 days ago

This is roughly what I do in Rust. I use different static types for values based on how long they'll live. Temporary values get one type; cached values get another. The allocator allocates each value in a different location based on how long the value will live.

Comment · 6 days ago

Yeah, that looks like a freelist approach. That will work as long as the values you're allocating are all fixed-size. You'll need something much more complicated if you want arbitrarily sized values

That example implements a linked list of integers. I'm curious how you would do a linked list of strings