That is trivially obvious, but writing a performant vector implementation is not solving the halting problem.

Let me restrict it to the faintly weaker "I hope we don't settle for unsafe being okay forever where we can prove safety".