[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <15c994fc-e638-4467-81d1-7d1e6e3c21c1@proton.me>
Date: Wed, 13 Dec 2023 23:51:31 +0000
From: Benno Lossin <benno.lossin@...ton.me>
To: Andrew Lunn <andrew@...n.ch>, 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, wedsonaf@...il.com, aliceryhl@...gle.com
Subject: Re: [PATCH net-next v10 1/4] rust: core abstractions for network PHY drivers
On 12/14/23 00:40, Benno Lossin wrote:
> On 12/13/23 22:48, Andrew Lunn wrote:
>>> 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?
>
> That is an interesting suggestion, do you have any specific tools in
> mind?
> There are some Rust tools for formal verification, see
> https://rust-formal-methods.github.io/tools.html
> but I don't know if they can be used in the kernel, especially since we
> would need a tool that also supports C (I have no experience/knowledge
> of verification tools for C, so maybe you have something).
> Also my experience tells me that there are several issues with formal
> verification in practice:
Don't get me wrong, I would welcome a more formalized approach. I just
have seen what that entails and I believe Rust (with safety comments)
to be a good compromise that still allows programmers with no knowledge
in formal systems to program and reasonable correctness.
> 1. When you want to use some formal system to prove something it is
> often an "all or nothing" game. So you will have to first verify
> everything that lies beneath you, or assume that it is correctly
> implemented. But assuming that everything is correctly implemented is
> rather dangerous, because if you base your formal system on classical
> logic [1], then a single contradiction allows you to prove
> everything. So in order for you to be _sure_ that it is correct, you
> need to work from the ground up.
>
> 2. There is no formal Rust memory model. So proving anything for
> interoperability between Rust and C is going to be challenging.
>
> 3. The burden of fully verifying a program is great. I know this, as I
> have some experience in this field. Now the programmer not only needs
> to know how to write a piece of code, but also how to write the
> required statements in the formal system and most importantly how to
> prove said statements from the axioms and theorems.
>
>
> When using safety comments, we avoid the problems of having to prove the
> statements formally (which is _very_ difficult). Of course people still
> need to know how to write safety comments, which is why I am working on
> a standard for safety comments. I hope to post an RFC in a couple weeks.
> It will also make the safety comments more formal by having a fixed
> set of phrases with exact interpretations, so there can be less room for
> misunderstandings.
>
>
> [2]: You might try to work around this by using a paraconsistent logic,
This should actually be [1]:.
> but I have little to no experience with that field, so I cannot
> really say more than "it exists".
--
Cheers,
Benno
Powered by blists - more mailing lists