> But you don't need to fix anything year after year. You only need to fix each bug once.

I was talking at a language meta-level, not for a particular program.

> But correct untouched code is correct regardless of the language used to write it.

A tautology, but largely irrelevant to the discussion, as if we could easily determine correct for anything other than the most trivial code, then this would be a non-issue. In practice, C has ended up being a poor choice for attempting to write correct code, as evidenced by the last few decades.

> Do you honestly think that the benefits of rewriting mostly correct, mostly untouched code in a new language is the best use of those resources? Do you even think that's the most cost-effective way of catching bugs (if so, I don't think you're aware of the capabilities of modern verification tools)?

The good thing is it doesn't matter. If it's done a little, and seems effective and is prized by users (users being both developers and end users), then it will happen. There isn't some central authority of programming that we need to make a case to, there's a free market to feel around the edges of the problem, and emergent behavior to actually make a choice. The good thing is that I think on average it's a few magnitudes more likely to make a good choice than anyone here as to what's the more useful and effective way to move forward.

> I think we're talking about at least a 10x larger effort, possibly 100x, but we won't know until we measure the correctness of said code to the best of our abilities using tools that can approximately do that rather effectively.

I don't think it's anywhere near that high, given the level both languages operate and and the similarity of the syntax. I think you would only approach those levels for more complex and esoteric pointer use, for small subsets of the code base, and we aren't measuring compared to rewriting in a language with the exact same capabilities, we're measuring compared to C with special analyzers and techniques used to reduce or remove problems, which I though would more than likely require a rewrite of those sections anyway to see any benefit.

> External tools are always necessary if you want to improve correctness, regardless of the language you use. Rust (and virtually every industry language out there) cannot prove most interesting functional properties, either.

That is easily proven false. Rust can be seen as a language that does not enforce memory correctness with a memory correctness tool bundled into the compiler. All the tools for C could be bundled into the compiler and a new language called Cfoo could be defined by what that supports. Every external tool can be bundled into the compiler (or the runtime, as applicable, by the compiler including it in the generated binary or its existence as part of the VM).

In the end, the same arguments regarding correctness apply to varying degrees to things written in assembly, and even raw machine code. We could be applying varying levels of analysis techniques to our assembly at this point, but a shift happened in the past when people saw languages that provided enough benefits that they saw the point of switching. That we mostly settled on C and haven't moved past it yet (depending on how much you consider C++ a C, and how incremental you see the changes) is largely an artifact of momentum, I don't think we should be discouraging people from trying to make that jump out of C for our infrastructure. I think that's the equivalent of you or I sitting in our comfortable homes and offices, carpeted, heated, sturdily built out of wood, steel and concrete, and noting that yes, while the majority of people either work or live in mud huts, it's a waste of resources for them to attempt to replace them with more modern housing when they can just retrofit their mud huts with a heater and portable stove and will be just as "serviceable". The best people to assess whether it's worthwhile or not are those doing the work, not you or I.