Re: Rust kernel policy

Ventura Jack
2025-02-22T17:10:53Z

On Sat, Feb 22, 2025 at 9:04 AM Kent Overstreet
<kent.overstreet@linux.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.

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.

The type systems and compilers of Haskell
and Scala look more robust to me. But, they
are reliant on GCs, making them irrelevant.
They also do not have affine types and borrow
checking as far as I know, unlike Rust, though
they may have experiments with it. Scala does
have dependent types.

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.

For anyone curious about the compile times and
type system issues, there are these examples:
https://github.com/lcnr/solver-woes/issues/1
https://github.com/rust-lang/rust/issues/75992

Best, VJ.