For some context, Ralf is one of the people who's been working on proving Rust code, and specifically unsafe Rust code. He's already had some really impressive results.
One of the weakest areas of Rust (in some sense) is unsafe; we don't have a proper understanding of what exactly is acceptable with unsafe code. Projects like these are working on proposing a model for what those rules should be.
So, if you're most Rust programmers, this doesn't affect you, really, other than making code you depend on a bit higher quality :). If you're an author of unsafe Rust code, this would tell you what you can and can't do, and if you work on a compiler, these rules would tell you what you can and can't optimize.
Additionally, this is pretty neat:
> I hope to explore this question further in the following weeks by implementing a dynamic checker to test the model on real code.
If we accepted this model (which is, of course, a big if; it was just proposed!), then we could take this tool and instrument your unsafe, an "unsafegrind", if you will, that could tell you at runtime if your code trips UB.
This tooling is enabled by MIRI, which is also amazing, but I've gone on too long already. TL;DR: it's sort of a "rust interpreter" that we've invested in for compile-time function evaluation, but also pays off with things like this.
One of the weakest areas of Rust (in some sense) is unsafe; we don't have a proper understanding of what exactly is acceptable with unsafe code. Projects like these are working on proposing a model for what those rules should be.
So, if you're most Rust programmers, this doesn't affect you, really, other than making code you depend on a bit higher quality :). If you're an author of unsafe Rust code, this would tell you what you can and can't do, and if you work on a compiler, these rules would tell you what you can and can't optimize.
Additionally, this is pretty neat:
> I hope to explore this question further in the following weeks by implementing a dynamic checker to test the model on real code.
If we accepted this model (which is, of course, a big if; it was just proposed!), then we could take this tool and instrument your unsafe, an "unsafegrind", if you will, that could tell you at runtime if your code trips UB.
This tooling is enabled by MIRI, which is also amazing, but I've gone on too long already. TL;DR: it's sort of a "rust interpreter" that we've invested in for compile-time function evaluation, but also pays off with things like this.