> Rust can be seen as a language that does not enforce memory correctness with a memory correctness tool bundled into the compiler.
What you call "memory correctness" is extremely valuable, but isn't correctness (in the software verification sense). Correctness is an external property of an algorithm. There are very few languages that can even express correctness properties. Correctness means something like: "every request will retrieve the relevant user data"; not: "the request will not fail due to a dangling pointer reference".
> I don't think we should be discouraging people from trying to make that jump out of C for our infrastructure
But I'm not discouraging people to move out of the C infrastructure. I want people to write new infrastructure. I just think it's a waste of effort to rewrite old infrastructure in new languages. To use your analogy, people want to rebuild the same mud huts just out of better mud. I say to them: what do you want? Do you want better mud huts? Then reinforce what you have; it will be a lot cheaper. But if you want to build something from scratch, why not build something new? Why spend the development budget on what is essentially maintenance? I don't know if that would be worth it, but at least it seems more worthwhile than re-implementing 1960-70s design with 201x materials, when we can make sure those mud huts stand long enough until we do come up with something new.
> Correctness is an external property of an algorithm.
While true (depending on what you think I meant by correct in that context), it's largely irrelevant to my point. Any external tooling can be merged with the compiler or VM.
> I just think it's a waste of effort to rewrite old infrastructure in new languages.
As you've stated multiple times here. Can I get a few examples of what you mean? I suspect there's a mismatch in our interpretation of the meaning of that statement.
Where does taking a libc implementation and converting with light refactoring fall, given there exists no other implementation in rust?
What about a new libc implementation from scratch in rust, using rust, given that there exist (non-rust) libc implementations?
What about a new libc implementation from scratch in rust, when there exists another rust libc implementation that isn't just a conversion?
What about an SSL library conversion (OpenSSL or NSS)?
What about a new implementation of SSL that conforms to OpenSSL's API?
What about a new implementation of SSL functions that has a completely new API to achieve the same operations?
> Not so simple. There is a debate whether it's better to specify correctness in the language or externally.
What's a benefit of having an external tool for that compared to something built in? Nothing comes to my mind that wouldn't be better handled as a per-location way to turn specific rules on and off (similar to Rust's unsafe blocks).
> Probably not worth it. But how about writing a Rust standard library in Rust that doesn't implement libc's API?
Well, yeah, that would be a good thing, but it's largely irrelevant to my point. In this case libc is just a wildly popular library we are considering presenting a new version of (whether it be largely a "fork" and refactor into rust of an existing one or a new implementation).
> May be worth it, given OpenSSL's state and importance.
Then I don't really think we are in disagreement on the "rewrite everything in rust" stance, as much as how we interpret that statement is different. I take it as far less literal, and more of a shorthand for "let's get rust implementations of critical infrastructure built so we can have some assurance a certain class of bugs can be close to eliminated. If the initial version of that is in some cases a conversion, that's not optimal, but it does provide some benefit, increase the corpus of rust work to refer to, prove rust's capability in the problem space, and provide a springboard for future projects".
That's a far cry from "let's rewrite every line of billions of lines of C code into rust because we want to rewrite it all".
> What's a benefit of having an external tool for that compared to something built in?
Because 1/ building full specification power into the language may make it unnecessarily complex, and 2/ software verification and PL design often progress at different paces, so it's better to have them orthogonal. I
It is unclear how such a language should work, and certainly whether anyone has come up with a decent idea yet. For example, the general dependent type approach used by Coq and Agda (and Idris and ATS) doesn't seem to work well so far for software development. So, perhaps theoretically the two may one day be combined, but we don't know how to do it just yet. You can call it an open research question.
> 1/ building full specification power into the language may make it unnecessarily complex
In that case, I'm not sure how you square the school of thought that you can use these external tools to solve the problems of C, or that it's at least more cost effective than something new, like Rust. If it's unnecessarily complex, does it matter if it's compiler+external tool or compiler+integrated tool? I think the same argument cuts both ways, except that in C it just means the tool won't be used, so the software will be of lower quality.
> 2/ software verification and PL design often progress at different paces, so it's better to have them orthogonal.
Having some verification integrated does not preclude further verification techniques from being developed. Types are a verification technique, and they exist in both C and Rust (at different levels). I'm not sure why it's okay for C to have some included verification, but not for languages to evolve further in this vein.
> If it's unnecessarily complex, does it matter if it's compiler+external tool or compiler+integrated tool? I think the same argument cuts both ways, except that in C it just means the tool won't be used, so the software will be of lower quality.
I'm not arguing in favor of one approach over another. My original point in this thread was solely about legacy codebases that are well-established and are no longer under active development, hence your arguments about enforcements do not apply. Now I'm talking in general. I don't know what you mean by an integrated tool, but there is a difference between making a language able to specify programs (like Idris), which may make it very difficult to use, or using a language that is relatively easy to use, plus a specification language, that's also easy to use.
> I'm not sure why it's okay for C to have some included verification, but not for languages to evolve further in this vein.
Again, my original point was only about codebases that aren't heavily developed, like libc. A language like Rust should and will have external verification tools, too, because its type system isn't powerful enough to specify correctness, and that's a good thing (because we don't yet know how to build friendly type systems that are capable of that). All I said was that if the codebase is huge, and if it is established and largely correct, and if it is no longer being heavily maintained, and if the language has good verification tools, and if there are no tests that will catch new bugs you will introduce in the translation, then it is more effective and far cheaper to use those tools than to rewrite in another language.
I understand your original point (if I still don't agree entirely), I was addressing some topics you brought up as tangents. I understand a language will always develop external tools is used enough, but I don't think that precludes migrating tools that have proved themselves into a language if the trade-off is clearly a good one, or at least a good one for a subset of problems (I think Rust fits this description).
To take a different tack on why I think it's not a waste to focus on rewrites of well established, mature code bases, consider the following: Rust is young. There aren't a lot of projects out there using it (comparatively), and almost none in certain sub-areas where it is supposedly a good fit (low level systems programs). A good way to find pitfalls, develop best practices and idioms, and find the pain points of the language is to use it to reimplement a well known, mature, stable project and see how it turns out.
You can say "sure, but we shouldn't focus on just that!", which is true, but also a non-sequitur, as I'm not sure anyone is actually doing so, or even suggesting it be done exclusively that way. I know what you are arguing, I'm just not sure why you feel the need to argue it, since I don't see anyone actually holding a position opposite you (the "we need to rebuild every project in Rust" view).
> but I don't think that precludes migrating tools that have proved themselves into a language if the trade-off is clearly a good one, or at least a good one for a subset of problems
Sure.
> A good way to find pitfalls, develop best practices and idioms, and find the pain points of the language is to use it to reimplement a well known, mature, stable project and see how it turns out.
Sure. I said that if the goal is to experiment with Rust, then rewriting some old code is a good exercise. But if the goal is to improve the quality of ~50MLOC, there are cheaper, less risky approaches.
What you call "memory correctness" is extremely valuable, but isn't correctness (in the software verification sense). Correctness is an external property of an algorithm. There are very few languages that can even express correctness properties. Correctness means something like: "every request will retrieve the relevant user data"; not: "the request will not fail due to a dangling pointer reference".
> I don't think we should be discouraging people from trying to make that jump out of C for our infrastructure
But I'm not discouraging people to move out of the C infrastructure. I want people to write new infrastructure. I just think it's a waste of effort to rewrite old infrastructure in new languages. To use your analogy, people want to rebuild the same mud huts just out of better mud. I say to them: what do you want? Do you want better mud huts? Then reinforce what you have; it will be a lot cheaper. But if you want to build something from scratch, why not build something new? Why spend the development budget on what is essentially maintenance? I don't know if that would be worth it, but at least it seems more worthwhile than re-implementing 1960-70s design with 201x materials, when we can make sure those mud huts stand long enough until we do come up with something new.