[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <83511ed4-1fbe-4cf6-ba63-5f7e638ea2a1@lunn.ch>
Date: Wed, 13 Dec 2023 22:48:39 +0100
From: Andrew Lunn <andrew@...n.ch>
To: Boqun Feng <boqun.feng@...il.com>
Cc: FUJITA Tomonori <fujita.tomonori@...il.com>, alice@...l.io,
netdev@...r.kernel.org, rust-for-linux@...r.kernel.org,
tmgross@...ch.edu, miguel.ojeda.sandonis@...il.com,
benno.lossin@...ton.me, wedsonaf@...il.com, aliceryhl@...gle.com
Subject: Re: [PATCH net-next v10 1/4] rust: core abstractions for network PHY
drivers
> Well, a safety comment is a basic part of Rust, which identifies the
> safe/unsafe boundary (i.e. where the code could go wrong in memory
> safety) and without that, the code will be just using Rust syntax and
> grammar. Honestly, if one doesn't try hard to identify the safe/unsafe
> boundaries, why do they try to use Rust? Unsafe Rust is harder to write
> than C, and safe Rust is pointless without a clear safe/unsafe boundary.
> Plus the syntax is not liked by anyone last time I heard ;-)
Maybe comments are the wrong format for this? Maybe it should be a
formal language? It could then be compiled into an executable form and
tested? It won't show it is complete, but it would at least show it is
correct/incorrect description of the assumptions. For normal builds it
would not be included in the final binary, but maybe debug or formal
verification builds it would be included?
> Having a correct safety comment is really the bottom line. Without that,
> it's just bad Rust code, which I don't think netdev doesn't want either?
> Am I missing something here?
It seems much easier to agree actual code is correct, maybe because it
is a formal language, with a compiler, and a method to test it. Is
that code really bad without the comments? It would be interesting to
look back and see how much the actual code has changed because of
these comments? I _think_ most of the review comments have resulted in
changes to the comments, not the executable code itself. Does that
mean it is much harder to write correct comments than correct code?
Andrew
Powered by blists - more mailing lists