-
Agreed! MIRI is so good, it still feels like magic to me. It also comforts me that the Rust team takes improving unsafe semantics seriously, with the past Unsafe Code Guidelines WG and today's operational semantics team (t-opsem).
-
SaaSHub
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
-
Agreed! MIRI is so good, it still feels like magic to me. It also comforts me that the Rust team takes improving unsafe semantics seriously, with the past Unsafe Code Guidelines WG and today's operational semantics team (t-opsem).
-
zig
General-purpose programming language and toolchain for maintaining robust, optimal, and reusable software.
But the author's complaint about Miri and aliasing is something I worry about quite a bit, and I think the author of this has drawn the wrong conclusion, sadly. Miri implements a prototype aliasing model, which is more restrictive than whatever will eventually be stabilized. If your code passes Miri that should generate significant additional confidence (but not prove!) that it does not run into any aliasing issues. But nothing of the sort can be said for Zig. The Zig language has an aliasing model, and it has aliasing UB. It must, because of the way it is implemented on top of LLVM, which deeply assumes that some classes of aliasing optimizations are valid. It is almost but not entirely certain that Zig has less aliasing UB than Rust, because that would fit with the language's general aim of making unsafe code easier to get right. And yet, there is no checker for aliasing UB in a Zig program. There is nothing beyond reading the code that I can do to generate confidence that a Zig program doesn't run into aliasing UB. So migrating off Rust on the basis that it is hard to satisfy Miri and to a language that doesn't have any kind of checker for aliasing UB is, at least in part, sticking your head in the sand.
