Ah, I should have clarified that. Yes, if stack overflow resulted in a trap you are mostly okay, given that the caller is eventually able to recover from the trap. But imagine that the trap didn't happen because the page table wasn't configured, like in the kernel context. Now your program will venture into some unintended memory region, yikes!
But that was about the general language-based security, and you are correct that this particular case wouldn't matter much for Cargo. I only used this example in order to show that fully verifying language-based security is very hard in general. Even Coq, a well-known proof verifier with a solid type theory and implementation, suffered from some bug that allowed `false` to be proved [1]. It's just that hard---not really feasible.
Yes, fine. Again, my north star is unsafe. Rust doesn't require that all code is safe. But it allows us to mark unsafe regions. I think that would get us pretty far.
If you want to prevent stack overflows, the compiler can calculate the maximum stack space needed by any call tree. (Well, so long as the code in question isn't recursive - but again, that could be enforced at compile time.)
That seems like something that could be checked statically. Alternatively, the kernel could dynamically allocate exactly the right amount of stack space for its own threads.
But that was about the general language-based security, and you are correct that this particular case wouldn't matter much for Cargo. I only used this example in order to show that fully verifying language-based security is very hard in general. Even Coq, a well-known proof verifier with a solid type theory and implementation, suffered from some bug that allowed `false` to be proved [1]. It's just that hard---not really feasible.
[1] https://github.com/clarus/falso