The Tower

> But that layer was a lie too, because beneath it there's the concrete reality of your hardware.

I'm afraid you are overstretching the "layer" analogy here. Yes, this can be described as a layer, too, *but it is a very different kind of layer from what Aria describes*.

All of Aria's layers are sound abstractions you can use in Rust. If you program using only safe high-level concepts, Rust promises that the resulting program will correctly follow the things you wrote. If you program using the weak memory model and strict provenance, Rust still promises that. But programming with the hardware model *is not possible directly in Rust* (or other, similar languages such as C and C++). Between you and the hardware, there is an optimizing compiler, and this compiler makes uninitialized memory and provenance a dead-serious reality that you have to live with. It's not a lie, it's real and can make your code go wrong. It's only real as an abstraction, as emergent behavior, but when you write Rust that is the abstraction you have agreed to use, as you better treat it as real. (I have a blog post about that at https://www.ralfj.de/blog/2019/07/14/uninit.html.)

If you have to use hardware-level reasoning, that's what inline assembly is for. (But getting the two to co-exist is a complicated topic.)

I think the common sentiment in low-level programming of treating the Rust (or C) Abstract Machine as somehow "not real" is dangerous. Obviously, the kernel is very prone to this kind of thinking since it is such low-level code, and the common sentiment of language designers of treating the Rust (or C) Abstract Machine as all there is is equally dangerous. The reality of hardware and things outside Rust (such as page tables, to name but a trivial example) is omnipresent. At the same time, though, this code is being compiled by an optimizing compiler, so the Rust AM is just as real as the hardware -- neither of them can be disregarded as a "lie", and a correct kernel can only be produced by treating both of these layers as real in their own right, and carefully managing the interaction between them.