Re: C aggregate passing (Rust kernel policy)

[Ralf Jung]

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