> First, a fixed bug is a fixed bug. You never ever have to rewrite a function that's correct. Second, the whole point of at least first trying to find the bugs, is that the whole effort is orders of magnitude smaller. Doing the verification step first and the rewrite later is as cheap as just doing the rewrite, if not cheaper (because then you at least know what to rewrite).

I think that's backwards. If you rewrite in Rust then you probably fix bugs without noticing them. If you verify in C first and then rewrite, you have to redo the verification. If we think of the code we're verifying as data, then it's good practice to spend a bit of time getting the representation of the data right before trying to operate on it - that's usually more efficient than starting operating on it now and then changing the representation later.

> In that case, why translate now? Proving bug-freedom is so hard regardless of the language[1], that translating the code first to Rust saves you very little and is just wasted effort that could have gone into improving formal verification tools.

In the medium term: I think verification is much easier when the code is in a better form. (If nothing else translating to Rust will often give you much more concise code to verify). So as long as you're going to put in enough effort for it to be worth doing the translation, translating then analysing will get you a better return than analysing then translating. (Indeed if you analyse and then translate, a lot of your analysis may need to be redone).

In the longer term: I think we're never going to be able to (affordably) prove (general) C code correct. Which in turn means that any static analysis efforts in C will ultimately be wasted (because whatever partial verification we'll get from them won't carry over through translation of the code, and won't help us to translate it either). Whereas even if we're going to end up having to translate into some post-Rust language (and my suspicion is that we will), I think translating into Rust takes us a valuable distance along that path (because the end target language will look a lot more like Rust than like C).

> With all the automated test-generations and new static analysis tools out there, the first thing you reach for is a manual translation?

Yes. I think translation should be the first resort, because it obviates all the other approaches (if a property is guaranteed by the language then that's better than any amount of test coverage), and because better code makes subsequent analysis easier. (I'm certainly interested in automating it though).

> I partly agree, but I think that refactoring largely untouched, largely correct code for clarity is also a waste of (much!) effort.

There's a huge gap between largely correct and entirely correct. If we believe the latter is what we'll eventually need, then such refactoring is valuable - and if there's other work to be done on the same code, then it's usually cheaper to do that work after the refactoring rather than before. I agree that refactoring not driven by a requirement is a waste, and I think many businesses hold a belief (whether they express it this way or not) that they won't ever need 100% proven correctness. (I disagree because I believe technological and social changes in the near future will radically change the economics of hacking, but that's a fringe position that I don't expect to be able to convince business leaders of).