> 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.
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.