jandrewrogers 6 days ago

This is correct (and I am using “invalid” here in a semantic sense, it is still structurally valid). There are a number contexts in low-level systems code where a static proof is not possible even in theory, so there needs to be a way for code to inspect object validity at runtime. Process address space isn’t entirely private, external actors that your process doesn’t entirely control can modify it e.g. via DMA.

The C++ compiler largely assumes that such static proof is possible by default and has no way of knowing if it is not. To address this, the C++ language has added features for annotating objects to indicate that static proofs of state are not possible at compile-time (e.g. std::launder).

Database kernels are the most extreme example of this because most objects in the address space don’t own their memory address and the mechanism that temporarily puts an object at a particular memory address is not visible at compile-time. Consequently, object location and state has to be resolved dynamically at runtime.

1
sunshowers 6 days ago

Definitely agree that there's plenty of cases in systems code where static proofs are impossible. That makes it all the worse when you give up on static proofs in places where they are possible.