linux-kernel - Re: Rust kernel policy

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite for Android: free password hash cracker in your pocket

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <CAFJgqgTFoqH8kDquHjhKXCvsXrF-uoHo=bq52Fgv+MKePy4zhA@mail.gmail.com>
Date: Sat, 22 Feb 2025 10:10:40 -0700
From: Ventura Jack <venturajack85@...il.com>
To: Kent Overstreet <kent.overstreet@...ux.dev>
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 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.

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.