> I don't really understand this. The tools work better on C code right now, because some/most of them just don't support Rust at all. It's not a theoretical problem, but a real problem: C has better verification tools than Rust at this time; running many of them is far less costly than a rewrite; ergo -- we should run those tools before we rewrite to guide us as to what, if anything, is worth rewriting.
> And what if it costs 10-100x as much? Because that is very likely to be the case. But we won't know until we run the tools...
Do you agree that if one believes (as I do) that we'll inevitably need to rewrite sooner or later, then running those C verification tools is a wasted effort? They won't generate results that usefully carry-over post-rewrite, and they're only helpful in determining what to rewrite if there's a possible result that would convince one that code is good enough to be used without rewriting.
If your use case is "we need to cut the defect rate of this C code by 50% as a one-off" then sure, I can see static analysis tools and the like being the cheapest way to achieve that. I'm not convinced that's a realistic use case - the requirements that lead one to want to reduce the defect rate are likely to be recurring. I think it gets exponentially harder to do that in C. (I think it still gets exponentially harder in Rust, but with a smaller base - so an exponentially large advantage from a rewrite in the long run).
> Do you agree that if one believes (as I do) that we'll inevitably need to rewrite sooner or later, then running those C verification tools is a wasted effort?
Yeah. But, the software industry wasn't born yesterday, nor ten years ago nor forty. AFAIK, in the entire history of software (at least since the sixties), a rewriting project of established code of such magnitude has never been done. The Linux kernel (incl. filesystems), common drivers, and the runtime library, plus common libraries would come to about 20-50MLOC (possibly much more). Rewriting it all (forget about Windows and OSX) would cost at least $100M, and would probably last 5-10 years. That does not even include common runtimes that actually run most software today (JVM, Python, etc.). The total cost would probably exceed $1B and, like I said, the software industry has never, to the best of my knowledge, opted for this option before (GNU doesn't count because it was there nearly from the start and the codebases weren't established). So my question is, for that price and that timeframe, wouldn't it be better to build something new? I mean you're missing out on a lot just by not having a Rust API, and since you need to relearn everything, why not redesign while you're at it?
Sure - I suspect we won't rewrite to the same interfaces, but rather rewrite in a looser sense of writing new implementations of the functionality we need. (The most plausible path forward I see is using something like rust to write a bootable hypervisor and a library of low-level functions for use in unikernels). That said a lot of language runtimes rely on libc (often as one of a very small number of dependencies), so I think a port of musl could potentially be valuable.
> And what if it costs 10-100x as much? Because that is very likely to be the case. But we won't know until we run the tools...
Do you agree that if one believes (as I do) that we'll inevitably need to rewrite sooner or later, then running those C verification tools is a wasted effort? They won't generate results that usefully carry-over post-rewrite, and they're only helpful in determining what to rewrite if there's a possible result that would convince one that code is good enough to be used without rewriting.
If your use case is "we need to cut the defect rate of this C code by 50% as a one-off" then sure, I can see static analysis tools and the like being the cheapest way to achieve that. I'm not convinced that's a realistic use case - the requirements that lead one to want to reduce the defect rate are likely to be recurring. I think it gets exponentially harder to do that in C. (I think it still gets exponentially harder in Rust, but with a smaller base - so an exponentially large advantage from a rewrite in the long run).