It certainly works in my C programs. And Fil-C demos imply that this also works for a lot of other complex real world programs, i.e. a basic Linux distribution with libreoffice on top... So yes, I would say this just works. I agree that catching this at compile-time is better, and to some degree this also works: https://godbolt.org/z/sse74vK9o
Rust does not offer compile-time guarantee that an out-of-bounds access does not panic either.
Agreed on the last point. I'm very much in favour of developing an analysis that can assert the absence of an abort, I just can't see how an approach like Fil-C can achieve that.
It can guarantee a potential memory corruption event will be caught at runtime, but at that point I have very limited options.
To be clear, I prefer aborting safely to corrupting memory. But I prefer "issue detected at development time" significantly more than both.