Comment by throwawaymaths
2 days ago
you're arbitrarily drawing the line where memory safe is. i could say rust is memory unsafe because it allows you to write code in an unsafe block. or you could lose memory safety if you use any sort of ~ECS system or functionally lose memory "safe"ty if you turn a pointer lookup into an index into an array (a common strategy for performance, if not to trick the borrow checker).
what you really should care about is: is your code memory safe, not is your language memory safe.
and this is what is so annoying about rust evangelists. To rust evangelists it's not about the code being memory safe (for example you bet your ass SEL4 is memory safe, even if the code is in C)
you wanna verify all your c just for memory safety? i bet you if you actually tried to verify c for memory safety, you would come screaming back to rust.
and also seL4 is about 10k lines of code, designed around verification, sequential, and already a landmark achievement of verification. linux is like 3 orders of magnitude more code, not designed around verification, and concurrent.