> If you cannot automatically annotate the code there is no point in trying as you can't do it manually.
How can you know this without a "viral" analysis that tells you how much annotation is needed, and where? Perhaps the code factors out all the low-level, "memory unsafe" hacks to its own module, and that can be feasibly annotated. It's just not something we can know in advance.