Message-ID: <qh7r6vpnmegxf6ofro2axhewt5ojntesxrlqs7vguo7tjc6gy6@4cucfg233kf7>
Date: Sat, 22 Feb 2025 12:34:35 -0500
From: Kent Overstreet <kent.overstreet@...ux.dev>
To: Ventura Jack <venturajack85@...il.com>
Cc: Greg KH <gregkh@...uxfoundation.org>, 
	Boqun Feng <boqun.feng@...il.com>, "H. Peter Anvin" <hpa@...or.com>, 
	Miguel Ojeda <miguel.ojeda.sandonis@...il.com>, Christoph Hellwig <hch@...radead.org>, 
	rust-for-linux <rust-for-linux@...r.kernel.org>, Linus Torvalds <torvalds@...ux-foundation.org>, 
	David Airlie <airlied@...il.com>, linux-kernel@...r.kernel.org, ksummit@...ts.linux.dev
Subject: Re: Rust kernel policy

On Sat, Feb 22, 2025 at 10:10:40AM -0700, Ventura Jack wrote:
> On Sat, Feb 22, 2025 at 9:04 AM Kent Overstreet
> <kent.overstreet@...ux.dev> wrote:
> >
> > On Wed, Feb 19, 2025 at 06:39:10AM +0100, Greg KH wrote:
> > > Rust isn't a "silver bullet" that will solve all of our problems, but it
> > > sure will help in a huge number of places, so for new stuff going
> > > forward, why wouldn't we want that?
> >
> > The big thing we run into when trying to bring this to a practical
> > systems language, and the fundamental reason the borrow checker looks
> > the way it does, is Rice's theorem. Rice's theorem is a direct corollary
> > of the halting problem - "any nontrivial property of a program is either
> > a direct consequence of the syntax or undecidable".
> >
> 
> How do runtime checks play into Rice's Theorem? As far as I know, Rust
> has or can have a number of runtime checks, for instance in some of
> the places where a panic can happen.

Rust can't do full theorem proving. You can do quite a bit with the
borrow checker and other type system enhancements, but you definitely
can't do everything.

So if the compiler can't prove something at compile time, you may need a
runtime check to avoid undefined behaviour.

And the fact that Rust eliminates undefined behaviour in safe code is
huge. That's really a fundamental prerequisite for anything that would
be meaningfully better than C, and Rust gets that right.

(which required the borrow checker, because memory safety = UB...)

That means that even if you don't know if your code is correct, it's at
least going to fail in predictable ways. You're going to get meaningful
backtraces, good error messages if you weren't horribly lazy (the Rust
Display trait makes that a lot more ergonomic) - that means no more two
week bisect + bughunts for a UAF that was silently corrupting data.

We _just_ had one of those. Just the initial bisect (and it turned out
to be in the fuse code) interrupted the work I and a user were doing to
test bcachefs fsck scalability for a full week, when we'd just dedicated
and setup a machine for that that we only had for a limited time.

That sucked: there's a massive hidden cost to the sorts of heisenbugs
that C allows.

Of course higher level logic errors could still result in a silent
data corruption bug in Rust: intelligent thought is still required,
until we climb the next mountain, and the next mountain, until we do get
to full correctness proofs (and then we still have to write the code).

> The type system holes in the Rust type system, and the bugs in rustc's
> solver, grates me a bit. A lot of hard work is done in Rust language
> land on fixing the type system holes and on a new solver for rustc
> without the issues of the current solver, while maintaining as much
> backwards compatibility as possible. Difficult work as I gather. The
> alternative GCC Rust compiler, gccrs, is (as I gather) planned to also
> use the new solver once it is ready. There were some versions of
> rustc, also in 2020, where compile times for some production Rust
> projects went from fine to exponential, and where it took some
> compiler work to mitigate the issues, due to the issues being related
> to holes in the type system.

I don't expect such issues to affect us normal kernel developers much.
Yes, the compiler folks have a lot to deal with, but "can it build the
kernel" is an easy thing to add to their automated testing pipeline.

And it's not like we never have to deal with compiler issues now.

> The more complex a type system checker and solver, the more difficult
> it can be to avoid holes in the type system and bugs in the solver.
> Hindley-Milner is great, also because it is relatively simple, and has
> proofs for it and its algorithms for type checking. Mainstream
> programming languages inspired by ML/Hindley-Milner do generally
> extend its type system, often to provide more flexibility.

If you want a real mental trip, consider that a type system powerful
enough for theorem proving must itself be turing complete (not
inherently, but in practice), and thus the halting problem applies to
"can the compiler even process its inputs without terminating?".

But compiler folks have been dealing with such issues for years already,
that's their ballgame.

Powered by blists - more mailing lists