3 ms·
There is a convert-Rust-to-Lean-for-verification project. The not-aliasing guarantees did help tremendously there. https://kha.github.io/2016/07/22/formally-ve
by qznc 10y ago
There is a convert-Rust-to-Lean-for-verification project. The not-aliasing guarantees did help tremendously there.
https://kha.github.io/2016/07/22/formally-verifying-rusts-binary-search.html https://kha.github.io/2016/07/22/formally-verifying-rusts-bi...
- tom_mellior 10y agoMy reading of that is that everything is made immutable, at which point aliasing isn't an issue anymore. I might be wrong though.
- derkha 10y agoAuthor of that project here, it's the other way around - I'm using the absence oft aliasing to turn mutable Rust code immutable, which I can then embed in Lean. But you're right that ownership (ie, affine types) per se doesn't help.