Re: C aggregate passing (Rust kernel policy)

Ventura Jack
2025-02-26T16:50:59Z

On Wed, Feb 26, 2025 at 9:10 AM Ralf Jung <post@ralfj.de> wrote:
>
> Hi,
>
> >> [Omitted] (However, verification tools are
> >> in the works as well, and thanks to Miri we have a very good idea of what
> >> exactly it is that these tools have to check for.) [Omitted]
> >
> > Verification as in static verification? That is some interesting and
> > exciting stuff if so.
>
> Yes. There's various projects, from bounded model checkers (Kani) that can
> "only" statically guarantee "all executions that run loops at most N times are
> fine" to full-fledged static verification tools (Gillian-Rust, VeriFast, Verus,
> Prusti, RefinedRust -- just to mention the ones that support unsafe code). None
> of the latter tools is production-ready yet, and some will always stay research
> prototypes, but there's a lot of work going on, and having a precise model of
> the entire Abstract Machine that is blessed by the compiler devs (i.e., Miri) is
> a key part for this to work. It'll be even better when this Abstract Machine
> exists not just implicitly in Miri but explicitly in a Rust Specification, and
> is subject to stability guarantees -- and we'll get there, but it'll take some
> more time. :)
>
> Kind regards,
> Ralf
>

Thank you for the answer. Almost all of those projects look active,
though Prusti's GitHub repository has not had commit activity for many
months. Do you know if any of the projects are using stacked borrows
or tree borrows yet? Gillian-Rust does not seem to use stacked borrows
or tree borrows. Verus mentions stacked borrows in "related work" in
one paper. On the other hand, RefinedRust reuses code from Miri.

It does sound exciting. It reminds me in some ways of Scala. Though
also like advanced research where some practical goals for the
language (Rust) have not yet been reached.

Best, VJ.