Reminder: unless your entire compiler toolchain is formally verified (it's not), you have no guarantees that the code it emits is memory-safe.
Language builtin collections in memory-safe languages are no different from rust's unsafe-using stdlib collections.
Conversation
seL4 actually uses an ordinary toolchain (gcc), not a formally verified one like CompCert; but then they prove their safety properties on the resulting assembly. unusual and interesting approach.
1
14
for some reason I thought seL4 specifically used CompCert, now I'm even more intrigued
I guess this explains why CompCert docs talk about PPC heh
1