The Tower

This idea of "acting outside of Rust's constraints" reminds me of Aria's "Tower of Weakenings" concept.

Aria talks about a tower - at the top of the tower are happy ordinary programmers, with a nice clean model of the world and everything works how they expected. This model is of course a lie, but it's a convenient lie and for huge numbers of software engineers it's more than adequate. In this model we never do anything "weird" like hide flag bits in a pointer, or mutate the same value from multiple threads without synchronisation, in Rust's safe subset we are prevented from doing such things by mistake by fiat.

One layer further down we've got an abstraction that's much more complicated and difficult to work with, this is where things like the Linux Kernel Memory Model and the C++ 11 Memory Model (roughly Rust's model) and such live. Aria's "Strict provenance" experiment lives in this layer, pointers have multiple components, including a "provenance" that is distinct from their physical representation on most real hardware. The compiler can't check we're obeying this model, however specialist tools can help verify our work is sound, as can review by other skilled programmers. Almost everyone who couldn't get what they needed in the simpler model above is satisfied here.

But that layer was a lie too, because beneath it there's the concrete reality of your hardware. For example "Out of Thin Air" values exist in that middle layer but not at the bottom. In the model unsynchronised arithmetic _could_ mean you get answers which depend on themselves, it's perhaps impossible to develop models that don't have this problem. But, it's also impossible to build concrete hardware with the behaviour that was so hard to eliminate in models. Down here, Aria's "Provenance" means nothing, there are no pointers, just addresses (on most hardware), and the addresses really are just bits. But also down here things like "variables" don't exist, there's no type system and Edsger Dijkstra's letter hasn't been received so they don't really have structured control flow. A total nightmare.

Clearly it's correct to strive for as many kernel programmers as possible to spend their time in the upper part of the tower, even in C this is less stressful.