fwiw at work we've been looking at what the options are more memory-safe kernels out there. Not many options. If there were a "safe linux" maintained by like canonical or redhat or whatever we'd use it. For datacenter workloads like sandboxes and virtualization I think it'd do well.

Kernel will eventually move to rust, but not the dramatic and fast way

Won't AI's ability to discover these bugs reduce the need to rewrite things in rust? If the major benefit to rewriting them is memory safety, I mean...

That's assuming the current models are able to find all the bugs, and that we won't have a better model out every few months that will be able to find even more obscure bugs.

We would also have to burn a trillion tokens a day verifying all the C code the hard way forever going forward. It would be cheaper to rewrite the kernel in Rust, subsystem and driver by driver at a time.

I see. Fair enough

That's a fair question, and actually one I ask myself too.

AI doesn't give a strong guarantee that things work though, while Rust gives a much stronger (not absolute) guarantee.

But maybe the way of the future is to auto-generate proofs that the code is memory safe. The C code and the AI generated proofs could live separately and so it would need less maintainer buy-in.

I'm thinking a language change isn't enough... At least not for a kernel.

There has to be a pseudo userspace type of way to build a kernel driver. Basically, user space programs are fine, but kernel drivers need their own form of encapsulation without expensive context switches.

Something like memory encryption or memory access bounds. During the handoff you do not change the address space, you just restrict access to a subset of the kernel memory.

You could in principle use LLM as a formatter, linter and a borrow checker, but an actual linter, formatter and rust compiler are still faster and cheaper to run on a million lines of code. They are more reliable too because of context size limits and attention thingy (read those thinking traces when it approaches 1M limit an fucks up tool calls -- you will get the sleep deprived person vibes from it).

So first you would run the three above to pick the low hanging fruit and then ask the shaitan in a box to find more bugs. Looking from another angle -- rust is another a tool AI can use to find memory bugs, so why not have rust.

Then again, I asked the thing to write some C (more or less from scratch) few weeks ago and the next time I looked it was chasing segfaults and wondering where they came from.

“Claude rewrite this project, its 40 million LOC, make no mistake”

> Just a prompt away, right?

Humans manually typing out the bytes of source code has been an outdated method, since around a year. It simply doesn't scale as much as those same humans directing agentic teams. So yes, it would be about prompts.

The hard part isn't the technology for the language transition, that one is present today. pgrust shows the way. It's ensuring maintainers are cooperative, i.e. a social problem. Eventually you diverge too much if you do a fork, so it's better done in cooperation with upstream.

Just check how long it took LLVM or GCC to switch off svn for example, and a language switch is much more involved than a VCS switch.

> pgrust shows the way.

You mean the pgrust which was recently caught for cheating benchmarks and incapable of even performing basic queries outside the benchmark set? Would love to see pgrust analysed by Jepsen like this other AI-generated, written in Rust, "formally verified" scam software.

https://jepsen.io/analyses/particledb-1.1.4

I think the pgrust controversy should be resolved now?

https://news.ycombinator.com/item?id=50209450

I don't consider a cheater downplaying their cheating to resolve the fact that they cheated, no. Every cheater has a defense when caught, and theirs was not convincing. At this point I think the only thing that could redeem their brand would be paying for a Jepsen analysis to verify pgrust is as good as they claim it is; I have zero reason to trust the words from the horse's mouth.

You don't have to take my word for it. The ClickHouse CTO (who opened the original removal PR) updated his post after reviewing our explanation and our fully open-source v0.4-beta submission[0]:

> We clarified with the author - while the binary had signs of optimization for specific benchmark queries, we have a reason to believe that the actual runtime didn't use per-query kernels... The usage of a query condition cache and cached statistics per granule is legitimate. The submission of a closed source preview version fine-tuned for benchmark was shady nevertheless. However, the new submission #2751 should move us post all the concerns.

Submitting an incomplete, closed-source preview build was a mistake on my part. Since then, we open-sourced a new version with full SQL support, ClickHouse merged it back into ClickBench, and the new version actually runs 7% faster (geomean) than the preview build that was removed.

[0] https://github.com/ClickHouse/ClickBench/pull/2165