4 ms·
Rust’s “mutable-xor-aliased” model makes it particularly amenable to developing verification tools on top of it [1]. Without this model, verification becomes ju
by arn3n 2y ago
Rust’s “mutable-xor-aliased” model makes it particularly amenable to developing verification tools on top of it [1]. Without this model, verification becomes just as hard — and just as practically intractable — as all the verifiers for existing languages.
1: https://graydon2.dreamwidth.org/312681.html https://graydon2.dreamwidth.org/312681.html
- porridgeraisin 2y agoThe link returns 403.
- johnisgood 2y agoIt (still) works for me.
- johnisgood 2y ago> Rust supports it better than many other imperative systems languages -- even some impure functional ones! I am surprised that this blog post does not mention Ada / SPARK at all though.
- gaugefield 2y agoWhile this does not mention it, in many other discussions Rust vs Ada is mentioned. My (late) introduction to Ada via was finding out in one of the Rust forums.
- throwawaymaths 2y ago> Without [mutable-xor-aliased], verification becomes just as hard i get graydons point but as a counterpoint: at the point where you're adding a verifier to X-lang, you might as well put mutable xor aliased in the verifier instead of in the compiler.