@yaelwrites it would be cool if there were any such low level languages available. Rust certainly makes claims that are at least partially true, but I find the lack of a clear definition of what they actually mean by memory safety to stand out as a red light.

@monad_cat @yaelwrites Yeah. I read through chunks of the Rust compiler some years ago looking for where those guarantees are made explicit. Seems that most of that is just assumed to be true as an implication of the syntax and no-reuse semantics. Which is probably true. But I haven't seen the proof.