> a question of whether that additional cost provides much vs just spending more putting guardrails around C/C++/etc with more formal methods/verifiers.

So the conclusion (or the closest you get to proposing an alternative strategy) is to just to pour more tens of millions down the black hole called Cartographing The Wild West of Pointers. Hardly pragmatic.