That greatly depends on how many memory-safe programs you want to prove are memory safe. If it's the same subset of programs that a language like Rust can prove

That greatly depends on how many memory-safe programs you want to prove are memory safe. If it's the same subset of programs that a language like Rust can prove to be memory-safe, the annotation overload need not be higher. If you want to prove that an arbitrary memory-safe C program is memory-safe, then, indeed, you'll likely need many more annotations. Even in those situations, adding more annotations or restructuring the code may be cheaper than a rewrite in another language. Sound static analysis for C is already not uncommon in some important domains.