Re: C aggregate passing (Rust kernel policy)

[Ventura Jack]

On Wed, Feb 26, 2025 at 7:14 AM Ralf Jung <post@xxxxxxxx> wrote:
>
> Hi all,
>
> > [Omitted]
> >
> > Are you sure that both stacked borrows and tree borrows are
> > meant to be full models with no false positives and false negatives,
> > and no uncertainty, if I understand you correctly?
>
> Speaking as an author of both models: yes. These models are candidates for the
> *definition* of which programs are correct and which are not. In that sense,
> once adopted, the model *becomes* the baseline, and by definition has no false
> negative or false positives.

Thank you for the answer, that clarifies matters for me.

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

Best, VJ.