This is important, because as much as some of us would like to nuke those languages, they aren't going away and plenty of domains are not going to move away from them anyway.
However there is only so much that one can improve without changing their semantics.
And if you start changing their semantics, then you end up with what is effectively another language, e.g. Checked C.
To speak of Frama-C specifically, it isn't competing with new languages like Zig and Nim, it's competing with rival tools like [0], and with SPARK Ada. Formal reasoning about code is, for now, a niche reserved for critical-systems development. That kind of work tends to use tried-and-true languages with tried-and-true tooling: C, C++, Ada, and occasionally even Java.
> the languages we did design would be designed to make it easy to make tools that help us use them.
This is already a factor in language design. It's one of the reasons C-style preprocessors are now unfashionable.