Memory safe languages aren’t about proving everything at compile time. Some version of a panic is going to be there, at a minimum for array bounds checking.

In Fil-C, if you don’t like the use after free panic, then just don’t call free and let the GC free your objects.

And if you’re doing safety critical stuff (I’m assuming that’s what you’re getting at) then the game is to prove that the system will be safe in the sense of not hurting people, not in the sense of memory safety. And that proof burden is much higher than the proof burden for memory safety.