Re: Rust kernel policy

[Kent Overstreet <kent.overstreet@linux.dev>]

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?

I would say that Rust really is a silver bullet; it won't solve
everything all at once but it's a huge advance down the right path, and
there's deep theoretical reasons why it's the right approach - if we
want to be making real advances towards writing more reliable code.

Previously, there have been things like Compcert (writing a compiler in
a proof checking language) and Sel4 (proving the behaviour of a (small)
C program), but these approaches both have practical problems. A proof
checker isn't a systems programming language (garbage collection is
right out), and writing correctness proofs for C programs is arduous.

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".

The halting problem states - "given an arbitrary program, you can't tell
without running it whether it halts or not, and then..." - you know.
Rice's theorem extends that: not only can you not tell if a program
halts or not, you can't tell in general anything about what a program
does without running it and seeing what happens.

The loophole is the "unless that property is a direct consequence of
the syntax".

"Direct consequence of the syntax" directly corresponds to static type
systems. This is the explanation for why large programs in statically
typed languages tend to be more maintainable than in python/javascript -
there are things about your program that you can understand just by
reading code, instead of running it and waiting to see what type a
variable has and what method is called or what have you.

IOW: improvements in static analysis have to come from type system
improvements, and memory safety in particular (in a language without
garbage collection) has to come from baking information about references
into the type system.

So this is why all those other "let's just add some safety features to C
or what have you" efforts are doomed to fail - for them to work, and be
as good as Rust, they'd have to add all the core difficult features of
Rust to C, and we'd still have to rewrite pretty much all of our code,
because making effective use of the borrow checker does require a fair
amount of rearchitecting and rewriting to make things more explicit and
more regular.

And Rust gets us a lot. Besides solving memory safety, the W^R rule of
the borrow checker gets us a lot of the nice "easy to analyze"
properties of pure functional languages, and it's a good foundation for
the next advances in formal verification - dependent types.

TL;DR - it's going to be worth it.

(Also, listen to people like Josef who say "I'm now writing Rust in my
day to day and I never want to go back". It really is that good.)