Re: C aggregate passing (Rust kernel policy)

[Ralf Jung]

Hi,

> > 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.

VeriFast people are working on Tree Borrows integration, and Gillian-Rust people 
also have some plans if I remember correctly. For the rest, I am not aware of 
plans, but that doesn't mean there aren't any. :)

> On the other hand, RefinedRust reuses code from Miri.

No, it does not use code from Miri, it is based on RustBelt -- my PhD thesis 
where I formalized a (rather abstract) version of the borrow checker in Coq/Rocq 
(i.e., in a tool for machine-checked proofs) and manually proved some pieces of 
small but tricky unsafe code to be sound.

> 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.

Yeah it's all very much work-in-progress research largely driven by small 
academic groups, and at some point industry collaboration will become crucial to 
actually turn these into usable products, but there's at least a lot of exciting 
starting points. :)

Kind regards,
Ralf