> generally eliminating the runtime checks you referred to.
Yes, but I conjecture that this may be largely irrelevant (and would love to hear an explanation of why my conjecture is false) because one of the following is true in a significant enough portion -- if not the majority -- of the cases where this applies, either: 1/ the proof of no overflow could be determined by a C tool (it may not be a 100% proof that works in the face of, say, concurrent modification like Rust can guarantee, but something that's more than good enough), or 2/ making full use of Rust's contribution in that regard would require an API change, which you can't do. In most other cases, utilizing Rust's contribution would require a careful, very expensive study and analysis of the code (if you don't want to introduce new bugs), and so in that case, too, a C rewrite of that particular piece may still end up being cheaper and not (significantly) less useful (as the rewrite would reshape the code in such a way that a C tool would be able to verify its correctness to a sufficient degree).
Remember that proof (and I don't necessarily mean formal proof) that a piece of C code is correct in some specific regard (overflow) is just as much a guarantee as having that property verified by the Rust compiler, and is just as useful if you don't intend to make changes to the code anyway. If you're writing new code, then obviously it's great having the compiler help you, but when seeking to correct bugs in old code, most of it is likely correct, the justification is different.
> I don't know anyone who is seriously advocating for "rewrite literally everything in Rust."
Then why are people arguing? I honestly don't think I wrote anything even slightly contentious in my original comment. I wrote something that I think is pretty obvious (and meant as an emphasis of what you've written in your post; certainly not to express disagreement) yet worth noting on HN, where some people may be too new-language-trigger-happy but may have less experience with legacy code improvement and various (effective!) verification tools, or may be unaware that the majority program-correctness work is done outside the realm of PL design.
Isn't it obvious that before deciding to rewrite large amounts of largely untouched and largely correct legacy code, we should weigh the relative cost and benefit of other approaches, like tools that can help find and fix lots bugs relatively cheaply, and then wrap the thing and forget about it until compelled to rewrite by some critical necessity? It seems like some people disagree, and favor a preemptive rewrite of as much infrastructure code as possible, merely because it's "better".
I admit I made the mistake of mentioning "totally correct" programs that, while true that they are currently more feasible in C than in Rust (thanks to really expensive tools like Why3 or even automatic code extraction from various provers), it is an entirely different and separate issue, one that applies only to a minuscule portion of software.
> Just that it's worth looking at how we might do so if we choose to, and that it's also useful to have exploratory projects which can discover some of the pitfalls here.
Absolutely. You're doing great work, and like I said, I hope you keep track of the effort you spend as well as the number and kind of bugs you find in the process. That would make your work truly invaluable.
> That would be absolutely fantastic! Because if that's happening, perhaps Rust will have improved the overall situation and encouraged using better typing guarantees for systems work.
Hmm, here we may be in disagreement. I think that making types ever more expressive has diminishing returns, and is, in general, not the best we can do in terms of correctness cost-effectiveness; indeed, most efforts in software correctness research look elsewhere. Types have some advantages when expressing more "interesting" program properties and some disadvantages (although I think Rust's borrow checking is some of the most useful use of advanced typing concepts I've seen in many years; I can't say the same about languages designed for industry use that try to employ general dependent types with interactive proofs).
> But for now, I think it's worth finding out what mileage we can get out of Rust and its various properties and guarantees.
I agree, but I believe more benefit will likely be gained by writing new libraries and programs, not from rewriting old ones. I think only concrete absolute necessity should guide any rewriting effort.
> I'm just choosing to spend a small amount of my free time exploring the possibility space of the Rust rewrite process so I can know more (and also learn more about how my OS and most applications work).
> Then why are people arguing? I honestly don't think I wrote anything even slightly contentious in my original comment.
I think your original interpretation was slightly pedantic, and even though, to your credit, you were very careful to repeat your exact phrasing multiple times in many comments, nobody commented on what was likely the crux of the difference (which I have to admit, I'm confuses as to why that was ignored). Should everyprogram be converted? Definitely not. Is conversion even necessarily the goal? I think not. I think the goal is to get a rust representative of each area for promote choice.
It's about trust, and not necessarily how much I trust the specific developer, but that in using a language the requires specific conformance to compile, I can replace some subset of the trust I had to afford to the developer to the tool I use to compile. Do I trust code written by DJB or the OpenBSD developers? Yes. Would I like a way to transfer some amount of that level of trust to the random author of a library on github that would be really useful for my work? Hell yes. Does that replace my need to look for markers, whether in the code or based on project/author status, to determine whether the project and/or developers are competent and trustworthy? No, but it can reduce it.
> I agree, but I believe more benefit will likely be gained by writing new libraries and programs, not from rewriting old ones. I think only concrete absolute necessity should guide any rewriting effort.
Depending on what you mean by "new libraries" (new concepts or new versions?), I don't think that's sufficient. True, most of the real benefit of a rewrite or new implementation of a need won't happen from a language conversion from an existing library, but if it comes down to getting a new (for example) libc and our choice is to convert a small implementation so there's something or to wait for the next project to come along and hope they don't choose C, I'm happy with the conversion for now. If we're lucky, it will also show those about to start on the next libc-like project that Rust is a viable option, so it isn't done in C.
Yes, but I conjecture that this may be largely irrelevant (and would love to hear an explanation of why my conjecture is false) because one of the following is true in a significant enough portion -- if not the majority -- of the cases where this applies, either: 1/ the proof of no overflow could be determined by a C tool (it may not be a 100% proof that works in the face of, say, concurrent modification like Rust can guarantee, but something that's more than good enough), or 2/ making full use of Rust's contribution in that regard would require an API change, which you can't do. In most other cases, utilizing Rust's contribution would require a careful, very expensive study and analysis of the code (if you don't want to introduce new bugs), and so in that case, too, a C rewrite of that particular piece may still end up being cheaper and not (significantly) less useful (as the rewrite would reshape the code in such a way that a C tool would be able to verify its correctness to a sufficient degree).
Remember that proof (and I don't necessarily mean formal proof) that a piece of C code is correct in some specific regard (overflow) is just as much a guarantee as having that property verified by the Rust compiler, and is just as useful if you don't intend to make changes to the code anyway. If you're writing new code, then obviously it's great having the compiler help you, but when seeking to correct bugs in old code, most of it is likely correct, the justification is different.
> I don't know anyone who is seriously advocating for "rewrite literally everything in Rust."
Then why are people arguing? I honestly don't think I wrote anything even slightly contentious in my original comment. I wrote something that I think is pretty obvious (and meant as an emphasis of what you've written in your post; certainly not to express disagreement) yet worth noting on HN, where some people may be too new-language-trigger-happy but may have less experience with legacy code improvement and various (effective!) verification tools, or may be unaware that the majority program-correctness work is done outside the realm of PL design.
Isn't it obvious that before deciding to rewrite large amounts of largely untouched and largely correct legacy code, we should weigh the relative cost and benefit of other approaches, like tools that can help find and fix lots bugs relatively cheaply, and then wrap the thing and forget about it until compelled to rewrite by some critical necessity? It seems like some people disagree, and favor a preemptive rewrite of as much infrastructure code as possible, merely because it's "better".
I admit I made the mistake of mentioning "totally correct" programs that, while true that they are currently more feasible in C than in Rust (thanks to really expensive tools like Why3 or even automatic code extraction from various provers), it is an entirely different and separate issue, one that applies only to a minuscule portion of software.
> Just that it's worth looking at how we might do so if we choose to, and that it's also useful to have exploratory projects which can discover some of the pitfalls here.
Absolutely. You're doing great work, and like I said, I hope you keep track of the effort you spend as well as the number and kind of bugs you find in the process. That would make your work truly invaluable.
> That would be absolutely fantastic! Because if that's happening, perhaps Rust will have improved the overall situation and encouraged using better typing guarantees for systems work.
Hmm, here we may be in disagreement. I think that making types ever more expressive has diminishing returns, and is, in general, not the best we can do in terms of correctness cost-effectiveness; indeed, most efforts in software correctness research look elsewhere. Types have some advantages when expressing more "interesting" program properties and some disadvantages (although I think Rust's borrow checking is some of the most useful use of advanced typing concepts I've seen in many years; I can't say the same about languages designed for industry use that try to employ general dependent types with interactive proofs).
> But for now, I think it's worth finding out what mileage we can get out of Rust and its various properties and guarantees.
I agree, but I believe more benefit will likely be gained by writing new libraries and programs, not from rewriting old ones. I think only concrete absolute necessity should guide any rewriting effort.
> I'm just choosing to spend a small amount of my free time exploring the possibility space of the Rust rewrite process so I can know more (and also learn more about how my OS and most applications work).
Awesome! Carefully collect data! We need it.