[jedbrown]

This is possible using branded indices.

https://plv.mpi-sws.org/rustbelt/ghostcell/paper.pdf https://gitlab.mpi-sws.org/FP/ghostcell/-/blob/master/ghostc...

[Joker_vD]

Yes, indeed. And it's not even a novel idea, my example is lifted straight from one of the references of the paper you've linked (namely, Kiselyov & Shan, "Lightweight Static Capabilities", 2007).

I personally think that taking an optimization (e.g. boundary checks elimination) and bringing it — or more precisely, the logic that verifies that this optimization is safe — to the source language-level is a very promising direction of research.