> With the former you lose all guarantees and fall back to a safe/unsafe duality
This is simply not true. The annotations are checked. It's exactly like adding type annotations when inference fails.
> with the latter you need to rethink how your code works to comply yo the analyzer's mindset
No. I'm talking about adding something like a bounds check in a function entry.
> in the end it's pretty much like Rust, but in an ad-hoc way, much less ergonomic.
Except that it is cheaper than a rewrite in Rust, which is one of the several reasons why this is currently the preferred approach in industry segments that require certain correctness guarantees. I don't know if you know this, but Rust isn't exactly making big headways in the safety/security-critical software world, especially, though not only, in embedded (for a multitude of reasons). Those sound static analysis tools, on the other hand, are showing nice growth.
Also, even if Rust were more ergonomic than this, there are alternatives that I think will be more ergonomic than Rust. I.e. it's not enough to be better than C++; if you want to get the people currently using C/C++ you need to be better than C/C++ in a way that justifies the transition cost and better than the other alternatives.
> You are well aware that this is not what “relatively easy” means.
Relatively easy means easier than all or most other available options. Anyway, that's what I meant.
> but the payoff is also lower in the long run (Rust offers more than zero-UB)
Nobody knows about the long term payoff Rust gives you because few people have had sufficient long term experience with it. It could be large, small, nil, or negative. And there are other languages as well. Zig, when it's available, might well have a bigger payoff than Rust (that's my current guess), and in any event, few people in the low-level programming space who aren't currently using C++ are even thinking about, let alone considering, Rust. Not that anyone is thinking about Zig, but at least Zig is aiming at C shops as well.
Again, as someone who has been using formal methods for some years now, I can tell you that nothing is obvious in software correctness, and no one knows what the best way to achieve it is (although we do know some best practices, and we have some answers to more specific questions).
> so we might get to a point (when tooling[1] and hiring pool have reached a point where it becomes sustainable) where the latter option makes more sense for most people
You are assuming that Rust is the preferrable choice. I no longer think it will be. BTW, here's "C2Zig": https://youtu.be/wM8vz_UPTE0