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