Hacker News Reader

Comment by pron | Hacker News Reader

While Rust can indeed provide great benefits over C in many respects (mostly security and safety, but also maintainability), rewriting "everything" in Rust, as the author says, is so monumental an effort that there is no chance of it happening, certainly not before a "better" language than Rust comes along (say, in another ten or fifteen years), and then what? Rewrite everything in that language?

A far more feasible approach (though still very expensive) -- and probably a more "correct" one, even theoretically -- is to verify existing C code using some of the many excellent verification tools (from static analysis to white-box fuzzing and concolic testing) that exist for C[1]. It is more "correct" because, while perhaps not providing some of the other benefits, those tools can prove more properties than the Rust type system can, and such tools don't (yet) exist for Rust.

Even if you want to write a green-field project today that absolutely must be correct, it's better to do so in C (or in some of the verified languages that compile to C, like SCADE) and use its powerful verification tools, than to write it in Rust. Verification tools are usually much more powerful than any language feature (even though Rust's borrowing system seems like it can prevent a lot of expensive real-world bugs). Of course, it would be optimal if we could do both, but the Rust ecosystem simply isn't there just yet.

This is part of a more general problem, namely that rewriting code in new languages -- any new language -- is so costly (and often risky, too), that the benefits are rarely if ever commensurate with the effort. This is why good interop with legacy libraries is so important (something, I understand, Rust does well), often much more important than most language features. Rewriting code is often the worst possible way to increase confidence in a library/program in terms of cost/benefit, both because verification tools are often more powerful than any language feature, as well as because new bugs are introduced -- either in the code or in the compiler (bugs that won't be uncovered by the usually incomplete legacy test suite, but would break some of the millions of clients). Rewriting is usually worth the effort if the codebase is about to undergo a significant change anyway, but almost never to increase confidence in the existing functionality.

EDIT: Clarification: if you're not going to use verification tools in your new project, anyway, than obviously using Rust would give you much better guarantees than C.

[1]: C and Java are the languages with the best collection of powerful verification tools (maybe Ada as well, but there's far less Ada code out there than C or Java).

View on HN

I don't buy the argument that verification using heavyweight verifiers is less expensive than rewriting in Rust. Formally verifying a piece of code is an enormous effort, while writing in Rust is usually less effort than the original unsafe code took to write, thanks to Rust's ergonomic improvements over C.

Besides, most safe languages for embedded use (SPARK, etc) get their safety by disallowing dynamic allocation, which is great for avionics systems and not so great for libc or any consumer or server software. (Or they use a garbage collector for the heap, which is not what you want for libc for the usual reasons.) Not coincidentally, the novel part of Rust's type system is the marriage of easy-to-use, zero-overhead C++-style dynamic allocation with the flexibility and safety of Cyclone-style region checking.

> while writing in Rust is usually less effort than the original unsafe code took to write, thanks to Rust's ergonomic improvements over C.

Absolutely, but do you think that rewriting billions of lines of C code in Rust is the best, most cost-effective way to increase confidence in them? Also, using verification tools can be done much more gradually (say, function by function) than rewriting in a new language (which may require a lot of ffi if done piecemeal), and there's no need to fear new bugs.

> Besides, most safe languages for embedded use (SPARK, etc) get their safety by disallowing dynamic allocation, which is great for avionics systems and not so great for libc or any consumer or server software.

True. I don't actually suggest using SCADE or SPARK for libc :) Astrée wouldn't work, either, as it also assumes no dynamic code allocation. But something like SLAyer (a tool by MSR based on proving separation logic properties through abstract interpretation) or Facebook's Infer should. I would guess that making those tools work well on more and more real-world code would be a much smaller undertaking than rewriting in Rust and proving no new bugs have been introduced.

I'm generally skeptical of significant, real-world, bottom line benefits new languages provide, but Rust has convinced me that, at least potentially, it can have some very significant benefits over C. But a wholesale rewrite of a near infinite amount of code, much of which may work well enough, plus the risk of adding new bugs in the process, without the means to detect them??? That's like draining the ocean with a spoon in the hope of finding a sunken treasure. Software engineers often speak of using the best tool for the job; rewriting vast amounts of code (with very incomplete test suites) in a new language is certainly far from the best tool for the job of increasing confidence in its correctness (unless a particular piece of code is buggy beyond repair).

Same goes for physical infrastructure, BTW. If your infrastructure is old and you fear some bridges may collapse, you inspect them all. You rebuild the crumbling ones and strengthen those with cracks. What you don't do is rebuild all the bridges in the country. That's not only wasteful and comes at the expense of new bridges you could have built, but may end up increasing the danger in some cases, rather than decreasing it.

A big part of writing about this was to share one potential strategy for reducing risk in rewrites by doing it function by function. That's a strategy which is available to Rust with zero overhead FFI, so I'm not sure why you're holding that up as a benefit exclusive to static analysis and verification tools.

Because -- and I may be wrong about this -- the FFI has zero runtime overhead, not zero coding effort overhead (i.e., FFI code isn't identical to native Rust code). So you'd want to rewrite again (the FFI code to native code) as you translate more functions.

How does that differ from what's been reported is extensive work to appease static analysis tools?

It differs by being a far more expensive (and probably less effective) way to achieve the goal. Those verification tools were designed to be spectacularly less expensive than a rewrite in a new language (which is often prohibitively expensive), or they wouldn't have been designed in the first place (they're all much newer than safe systems languages like Ada).

I said that using verification tools is expensive, but I'd be surprised if it's not at least one, if not two, orders of magnitude less expensive than a rewrite (I can think of few if any more expensive ways of increasing confidence in such large amounts of legacy code than rewriting it). It can provide similar -- sometimes worse, sometimes better -- guarantees, requires much less creativity, it automatically focuses you on places in the code that are likely to be buggy (or, alternatively, shows you which code is likely not buggy) and cannot introduce new bugs that you have absolutely no way of detecting before pushing the new code to production systems.

(BTW, the chief complaint against those tools -- and what makes them expensive to use -- is that they have too many false-positive reports of potential bugs, but even "too many" is far fewer than every line, which is what you'll need to consider and study when rewriting.)

I think that since you're making concrete claims about actual cost and benefit, perhaps it's appropriate to suggest that you cite some sources (postmortems, white papers, journal articles) which have found these assertions to be true?

You're suggesting that rewriting billions of lines of code that probably contain lots of bugs somewhere every time a new safer language comes along is the most sensible investment of effort by the software industry in order to improve the quality of our software infrastructure, while I'm saying, wait, maybe we should use some inspection tools first before we decide on an approach, so at least we know where the worst of the problem is, and you think I'm the one who needs to cite sources? Alternatively, do you think that "rewrite all legacy code!" (an effort that would probably cost billions of dollars) does not need to be justified by concrete claims about actual cost and benefit?

But fine, here's a taste (look for what is required to use the tool as well as results):

* http://mir.cs.illinois.edu/marinov/publications/SenETAL05CUT...

* http://lcamtuf.coredump.cx/afl/ (see the "The bug-o-rama trophy case")

* http://research.microsoft.com/pubs/144848/2011%20CAV%20SLAye...

* https://code.facebook.com/posts/1648953042007882

* http://link.springer.com/chapter/10.1007/978-3-319-17524-9_1

Note that there are some strengths, some weaknesses, but I hope those sources make it clear that using those tools first is at least more sensible than "rewriting everything", as they require orders of magnitude less effort, and they do uncover bugs (you're free to guess what percentage of those bugs would be found in a rewrite, and whether the bug density demands a rewrite). We may decide that a rewrite of some libraries is the best approach once we have more information.

Now, do you have any sources suggesting that a complete rewrite is cost-effective?

The biggest problem I (not being the people you've been conversing with so far, for the most part) have with relying on static analysis tools on top of C, instead of a rewrite, is that the analysis tools are not enforceable. You can do all the analysis you want, and put in all the procedures you want, but in the end people are submitting changes to these libraries, and you need to make sure that these people are ensuring the tools get run prior to release. Additionally, from the perspective of a user of this code, my ability to look at the source and know that it's been scanned ranges from uncertain to non-existent. Switching to a compilation system where these constraints are enforced (such as a new language that enforces it) has a benefit in that respect. You could get a similar benefit by releasing a specialized C compiler that enforced some static analysis tools and required a very small amount of syntax change such that the code would not compile on a vanilla C compiler, and then I think the there would be much less of a case for a rewrite in Rust from a safety point of view (even if they would handle slightly different aspects of safety, as you've pointed out).

That said, I'm not sure it makes sense to rewrite "everything" in Rust, but it would be nice to see one or two representatives of each thing in rust, so you can rely on the assurances Rust provides as much as possible as far down the stack as you can, if that's desired. In other words, I don't think we need every compression library ported to Rust, but I would like to see one or two choices for each type of compression, as applicable. An easy way to jump-start this is to take a library and port it.

1. We are not talking about code that is under heavy development. I specifically said that rewriting code may be sensible if you intend to make big changes.

2. Obviously, verification tools (and I'm not just talking about static analysis, but also whitebox fuzzing and concolic testing) do have their downside. The question is not which approach yields the best overall result, but which is more economically sensible given the goal.

> it would be nice to see one or two representatives of each thing in rust

Absolutely, as long as it's done while analyzing the cost vs. benefit. What isn't so nice is to have the software industry waste precious efforts rewriting instead of developing new software, without analyzing where a rewrite would yield the most benefit. Obviously, anyone is free to choose what they want to spend their time on, but I think that as an industry we should at least encourage projects with higher impact first.

> What isn't so nice is to have the software industry waste precious efforts rewriting instead of developing new software, without analyzing where a rewrite would yield the most benefit.

That's entirely subjective based on how short-term and long term your thinking is, and whether you think C will still be the dominant language for some things in 10 or 20 years.

I think C is a local maximum, it's already surpassed its limits as a language (as we're now talking about extra-language tools to enforce non-language constraints), and is approaching its potential limits. We can put X time in making it slightly better, and get closer to the asymptotic limit of C's capabilities, or we can spend some (small) multiple of that time to reimplement in something that is by its nature slightly more capable immediately, and with possibly much more future potential.

Fixing up the old Pinto year after year because it still works and gets you from here to there always looks like a good decision when you are just looking at your monthly outlay. But when you consider environmental impact, safety to yourself and those around you, and comfort, spending that extra money to get the new Focus starts to look really appealing. Sure, look at all that money you're throwing out by buying a newer car, but it's a fallacy to think you got nothing for it, and would have been just as well served by the Pinto. You mght have been, or tomorrow might have been the day you got in an accident. What would you rather be driving when that happens?

Note: This doesn't really mean that Rust needs to be the next thing, but I do think it's a fallacy to look purely and time spent when considering language rewrites, where there are so many important factors that ignores.

But you don't need to fix anything year after year. You only need to fix each bug once. If you decide to significantly modify the code or add new features -- by all means, rewrite if you think it's worth it. But correct untouched code is correct regardless of the language used to write it. And this is what we're talking about here: mostly untouched code. The limits of C as a language are entirely irrelevant, as the vast majority of this code interests us mostly in its machine representation. It's not under heavy development, so who cares what language it's written in if it's correct? And even if you do care, do you care enough to invest so much money to that particular end, money that could be invested elsewhere?

Do you honestly think that the benefits of rewriting mostly correct, mostly untouched code in a new language is the best use of those resources? Do you even think that's the most cost-effective way of catching bugs (if so, I don't think you're aware of the capabilities of modern verification tools)?

> or we can spend some (small) multiple of that time to reimplement in something that is by its nature slightly more capable immediately, and with possibly much more future potential.

I think we're talking about at least a 10x larger effort, possibly 100x, but we won't know until we measure the correctness of said code to the best of our abilities using tools that can approximately do that rather effectively.

> as we're now talking about extra-language tools to enforce non-language constraints

External tools are always necessary if you want to improve correctness, regardless of the language you use. Rust (and virtually every industry language out there) cannot prove most interesting functional properties, either.

> But you don't need to fix anything year after year. You only need to fix each bug once.

I was talking at a language meta-level, not for a particular program.

> But correct untouched code is correct regardless of the language used to write it.

A tautology, but largely irrelevant to the discussion, as if we could easily determine correct for anything other than the most trivial code, then this would be a non-issue. In practice, C has ended up being a poor choice for attempting to write correct code, as evidenced by the last few decades.

> Do you honestly think that the benefits of rewriting mostly correct, mostly untouched code in a new language is the best use of those resources? Do you even think that's the most cost-effective way of catching bugs (if so, I don't think you're aware of the capabilities of modern verification tools)?

The good thing is it doesn't matter. If it's done a little, and seems effective and is prized by users (users being both developers and end users), then it will happen. There isn't some central authority of programming that we need to make a case to, there's a free market to feel around the edges of the problem, and emergent behavior to actually make a choice. The good thing is that I think on average it's a few magnitudes more likely to make a good choice than anyone here as to what's the more useful and effective way to move forward.

> I think we're talking about at least a 10x larger effort, possibly 100x, but we won't know until we measure the correctness of said code to the best of our abilities using tools that can approximately do that rather effectively.

I don't think it's anywhere near that high, given the level both languages operate and and the similarity of the syntax. I think you would only approach those levels for more complex and esoteric pointer use, for small subsets of the code base, and we aren't measuring compared to rewriting in a language with the exact same capabilities, we're measuring compared to C with special analyzers and techniques used to reduce or remove problems, which I though would more than likely require a rewrite of those sections anyway to see any benefit.

> External tools are always necessary if you want to improve correctness, regardless of the language you use. Rust (and virtually every industry language out there) cannot prove most interesting functional properties, either.

That is easily proven false. Rust can be seen as a language that does not enforce memory correctness with a memory correctness tool bundled into the compiler. All the tools for C could be bundled into the compiler and a new language called Cfoo could be defined by what that supports. Every external tool can be bundled into the compiler (or the runtime, as applicable, by the compiler including it in the generated binary or its existence as part of the VM).

In the end, the same arguments regarding correctness apply to varying degrees to things written in assembly, and even raw machine code. We could be applying varying levels of analysis techniques to our assembly at this point, but a shift happened in the past when people saw languages that provided enough benefits that they saw the point of switching. That we mostly settled on C and haven't moved past it yet (depending on how much you consider C++ a C, and how incremental you see the changes) is largely an artifact of momentum, I don't think we should be discouraging people from trying to make that jump out of C for our infrastructure. I think that's the equivalent of you or I sitting in our comfortable homes and offices, carpeted, heated, sturdily built out of wood, steel and concrete, and noting that yes, while the majority of people either work or live in mud huts, it's a waste of resources for them to attempt to replace them with more modern housing when they can just retrofit their mud huts with a heater and portable stove and will be just as "serviceable". The best people to assess whether it's worthwhile or not are those doing the work, not you or I.

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

> Any external tooling can be merged with the compiler or VM.

Not so simple. There is a debate whether it's better to specify correctness in the language or externally.

> Where does taking a libc implementation and converting with light refactoring fall, given there exists no other implementation in rust?

Probably not worth it. But how about writing a Rust standard library in Rust that doesn't implement libc's API?

> What about a new implementation of SSL that conforms to OpenSSL's API?

May be worth it, given OpenSSL's state and importance.

> What about a new implementation of SSL functions that has a completely new API to achieve the same operations?

Go for it!

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

> You can do all the analysis you want, and put in all the procedures you want, but in the end people are submitting changes to these libraries, and you need to make sure that these people are ensuring the tools get run prior to release. Additionally

This sounds like a problem that's easily solved with tooling, including continuous integration and mandatory pre-release testing.

Tooling is specifically not the problem. Since you can't enforce the client runs the tooling, you can't ensure the code is actually conformant. You can put policies and tooling in place so that it should be, but there's no way to ensure it. If you're both the developer and the user, sure, you can get pretty close, but what about an open source project that's freely available? You aren't going to get anywhere close to making sure it's tested at most compiles, and if you can't ensure that, you can't really protect against something of someone subverting your tooling, on purpose or accident and getting non-conforming code in the repo.

> You're suggesting that rewriting billions of lines of code that probably contain lots of bugs somewhere every time a new safer language comes along is the most sensible investment of effort by the software industry in order to improve the quality of our software infrastructure

From my own post:

> ... there are a bunch of calls to just rewrite the world in Rust, but even given unlimited resources, is it actually a reasonable thing to do? How well can Rust actually replace C in C’s native domains? What are best practices for managing the risks inherent in a project like that (injecting new bugs/vulnerabilities, missing important edge case functionality, etc.)?

> I don’t really know good answers to these questions...

So I'm not sure exactly where you're getting that argument. This also isn't "every time a new safer language comes along," Rust (AFAIK) is one of very few languages which is generally usable, memory safe, and without a garbage collection.

> ... do you think that "rewrite all legacy code!" (an effort that would probably cost billions of dollars) does not need to be justified by concrete claims about actual cost and benefit?

Absolutely not. But I don't see anywhere that I or others are making that claim. Part of what interests me here is to explore possible avenues of these rewrites.

> so at least we know where the worst of the problem is

I think that CVE's already give us a pretty good idea of places we might start if we were to seriously undertake this endeavor (as opposed to the hobbyist exploration I've started).

> But fine, here's a taste (look for what is required to use the tool as well as results): ...

Some of these look quite promising (and I suspect most on HN are familiar these days with AFL), but the only one which purports to present a cost/benefit analysis or postmortem requires paying $30 for the chapter. I'm not saying that analysis tools are a bad thing (and I would argue are quite badly needed because no matter how badly we want to we could never rewrite "everything" in Rust). I'm not saying that they aren't useful, or that they don't improve existing projects. I'm just saying that I don't yet see evidence that they are strictly always more cost-effective for needed improvements than a safe-language rewrite. I just don't know. I think that the software community barely knows how to properly quantify these things, so it's no surprise that there aren't any good metrics for making these decisions.

> Now, do you have any sources suggesting that a complete rewrite is cost-effective?

It's a small part of what I'm investigating with this project, specifically with regard to Rust. I think that looking into techniques for managing risk in any project (whether the changes are happening due to static analysis warnings or do to a rewrite) is useful.

Although, regarding Rust, one company (MaidSafe, talk about this here: https://www.youtube.com/watch?v=t8z5rA3A1RA) has already reported very promising results from a C++ to Rust rewrite. Dropbox rewrote a core piece of their Magic Pocket infrastructure from Go to Rust to get a handle on memory usage and has also generally reported positive results (wired article: http://www.wired.com/2016/03/epic-story-dropboxs-exodus-amaz..., subsequent HN conversation with Dropbox engineers: https://news.ycombinator.com/item?id=11282948).

All that said, I wouldn't generally advocate for complete ground-up rewrites without an incremental plan. Which is why I'm experimenting with ways to do so successfully and ergonomically between C and Rust.

> From my own post: ...

I acknowledged what you wrote -- and emphatically agreed with it -- in my original comment. I'm not sure what we're arguing about here (I guess I attributed to you something that would disagree with what I had said).

> Rust (AFAIK) is one of very few languages which is generally usable, memory safe, and without a garbage collection.

Similar arguments could have been (and maybe were) made when Ada was introduced, and will be made again if and when ATS or Idris are ever production-quality. Every good new language -- like Rust and like Ada (though I have serious doubts about Idris/ATS) -- improves on its predecessors. But being better -- even much better -- does not imply that a rewrite of legacy code that is not undergoing regular maintenance is the best possible use of resources (even if it were the gold standard, which I'm not sure it is considering the risks involved on top of the effort). I'm convinced that Rust is better than C enough to warrant the effort of switching languages for new code in many, and maybe even most, C shops. But to rewrite legacy code that is not undergoing regular improvement?

> I think that CVE's already give us a pretty good idea of places we might start if we were to seriously undertake this endeavor

Great, then we're in full agreement. My only warning was about deciding to rewrite before weighing alternatives and without having a good handle on precisely where the effort would yield the greatest benefit.

> I'm just saying that I don't yet see evidence that they are strictly always more cost-effective for needed improvements than a safe-language rewrite.

First you need to know what those needed improvements are. Second, some of those tools require very little effort as opposed to a rewrite, which requires a lot of effort, as you pointed out so well. Wouldn't giving them a try first be a more sensible thing to do (if the goal is to improve the quality of legacy code, obviously not if the goal is an experiment in Rust)?

> Although, regarding Rust...

Both of these concern code that is under heavy active development, something that I specifically said may warrant a rewrite (hopefully after weighing alternatives).

> All that said, I wouldn't generally advocate for complete ground-up rewrites without an incremental plan. Which is why I'm experimenting with ways to do so successfully and ergonomically between C and Rust.

Excellent, which is why I agreed with your post and said so. If you want to make your interesting work more impactful on the industry, please keep track of every legacy bug you find in the process, as well as the number of hours you work and how it is broken down to tasks (learning, translating etc.). Such a report could be invaluable.

> and cannot introduce new bugs that you have absolutely no way of detecting before pushing the new code to production systems.

Yes, they can. Remember the Debian OpenSSH vulnerability that arose from blindly making changes that Valgrind suggested?

> It can provide similar -- sometimes worse, sometimes better

Much worse, unless you're talking about systems that verify memory safety problems by disallowing dynamic allocation.

> Those verification tools were designed to be spectacularly less expensive than a rewrite in a new language (which is often prohibitively expensive), or they wouldn't have been designed in the first place (they're all much newer than safe systems languages like Ada).

I don't agree. Are you talking about things like Coverity? Coverity hasn't effective at stemming the tide of use-after-free and whatnot.

I strongly encourage you to familiarize yourself with Rust's ownership and borrowing discipline and to understand how it prevents problems like use-after-free. You'll find that it's very hard to retrofit onto C, and that's why no practical static analyses do it.

> Yes, they can. Remember the Debian OpenSSH vulnerability that arose from blindly making changes that Valgrind suggested?

Obviously, I'm not suggesting to blindly make any code changes. But do you honestly think the risk is anywhere at the same level as rewriting the whole thing? At least concentrate the effort where there likely is a problem rather than everywhere.

> Much worse, unless you're talking about systems that verify memory safety problems by disallowing dynamic allocation.

No. I am talking about both tools that are designed to uncover errors somewhat similar to Rust (SLAyer, Infer) as well as tools like CUTE and American fuzzy lop, that have completely different strengths. The former may be much worse; the latter may be much better. But let me suggest this: how about using tools like CUTE or AFL to generate more tests first, just so you at least have a better idea of which code is more problematic than other? You're suggesting to rebuild every bridge before even conducting an inspection that would give you an idea about where most problems lie. Those tools have been proven to be effective (see a very partial list here: https://news.ycombinator.com/item?id=11891635) and they do require orders of magnitude less work than a manual rewrite (they require less effort than even reading the code, let alone translating it). Shouldn't they at least guide the effort, help us concentrate our force where it would yield the biggest advantage?

> I strongly encourage you to familiarize yourself with Rust's ownership and borrowing discipline and to understand how it prevents problems like use-after-free. You'll find that it's very hard to retrofit onto C, and that's why no practical static analyses do it.

I am familiar with Rust's borrowing and I absolutely fucking love it! It is freakin' awesome! I recommend it to every C/C++ developer, and I sing Rust's praises whenever I have the chance; I really (really really) do. I think that Rust is definitely one of the most significant contributions to systems programming in the past couple of decades (if not more), and it is one of the most interesting (and potentially significantly useful) languages of any kind. I love and admire what you've done. Just the other day I told a friend that I'm sad I don't do as much low-level system's programming as I used to just so that I could have a chance to closely work with Rust rather than merely admire it.

But that has little to do with what I'm saying. First, I am not saying that the two approaches would squash the same bugs (see above). Second, suppose you're right about your analysis of the quality of the result (even though I disagree, as above). The question is not which would yield a better result overall (and I might agree that a Rust translation would, if only by ensuring that every line of code out there gets read and analyzed) but whether the result is worth the undertaking, and whether the best, most cost-effective way to improve the safety/correctness of legacy code of unknown, probably widely uneven quality, with little to non-existent test coverage is by rewriting the whole thing whenever a new, safer language comes along. I must say that I am truly surprised that you suggest that to be the most worthwhile, economically reasonable approach. Rebuilding every bridge when a stronger building material is invented really is terrific (provided that the work is infallible); but is that the most economically sensible approach to improve infrastructure? Isn't the effort best spent elsewhere?

I agree that Rust is superior solution if we're talking use-after-free detection. Also agree on tool immaturity. However, recent results might make you reconsider how practical they are.

http://research.microsoft.com/en-us/um/people/marron/selectp...

https://dl.acm.org/citation.cfm?id=2662394&dl=ACM&coll=DL&CF...

IMDEA's Undangle seems to have nailed it totally with one other doing pretty good. You're the compiler expert, though. Does Undangle paper seem to be missing anything as far as UAF detection or is it as total as it appears?

What I think is relevant in this case is not whether an an external tool for C can reach the same levels of safety presented by Rust, but whether an external, optional tool will every be able to provide the same level of assurance given that you can't ensure confirmity on the (source) consumer end without getting all the same tools and rerunning them (which is the situation you have when it's built into the compiler.

Another way of stating this is "code verification tools for C are great! What level of market penetration do you think we can achieve? Oh. That's disappointing..." :/

That's a great point but a bit orthogonal. It's very important if one is aiming for mass adoption. Hence, why C++ was built on C and Java combined a C-like syntax with a marketing technique I call "throw money at it." We still need to consider the techniques in isolation, though.

Here's why. One type of tool needs to either not force conformity or blend in seemlessly with everyone's workflow with wide adoption due to awesome compatibility, safety, efficiency, and price tradeoffs. That's HARD. The other is just there for anyone that chooses to use it recognizing value of quality in a lifecycle. It just needs to be efficient, effective, have low to zero false positives, work with what they're using, be affordable, and ideally plug into an automated build process. These C or C++ techniques for safety largely fall into category number 2.

I totally agree with you on overall uptake potential. There's almost none. Most of the market ends up producing sub-optimal code with quality non-existent or as an after-thought. Those that do quality in general follow the leader on it. It's a rare organization or individual that's carefully researching tools, assessing their value, and incorporating everything usable into the workflow. Nothing I can really do about this except push solutions that are already mainstreaming with the right qualities. Rust, Go, and Visual Basic 6 [1] come to mind.

[1] When hell freezes over...

I would say this is more like a new building material coming along which allows infrastructure to be built that results in a safer construct. No, you don't want to rebuild everything at once, and maybe you never want to rebuild everything, but sometimes old but serviceable things may be considered for replacement because not only can it be made safeer, but there may be other benefits at the same time (less room, more likely to withstand 1 in X type natural disasters, etc.).

Additionally, I never took the "rewrite everything" camp, as presented here, to really mean "everything" as much as to mean "a stack from the bottom up so there are rust versions to use". Java seems has a lot of this, by virtue of being a contained system that doesn't like to share it's memory, so there are Java versions of just about everything. Rust can use C with zero cost runtime cost, I think people just want to make it so that rust must use C for certain things.

> It is more "correct" because, while perhaps not providing some of the other benefits, those tools can prove more properties than the Rust type system can

Such as? And in that case, why not lift them into a language type system?

When working on code where particular properties are verified, it's very useful if all the tools share a common understanding of those properties. If you write something in Rust, your IDE will understand the types (and make sure to preserve them when doing automated refactoring), your debugger will know which preconditions were supposed to be semantically impossible, and so on. Last time I looked at external verification tools for C-like languages you often ended up having to explain the same fact twice to two different verification tools with overlapping featuresets, yet alone getting any help from other tools. If we're going to reach critical mass on safety tooling, it will have to be via a commonly understood specification that's a de facto language definition.

So given we're creating a new safe language, what parts of C would we actually want to keep? The lengthy operator precedence table? The preprocessor, and the absence of any module system? The extensive array of language-level operators for doing a wide variety of arcane bit-twiddling operations? The signed/unsigned arithmetic promotion rules that even experts misread? The implicit conversions between arrays and pointers? The lack of any sum (tagged union) type? The for loop that makes arithmetic - or, indeed, arbitrary code - first class, and iterating over an array or other collection something you hand-code every time?

Even if it were as safe as Rust, C would still be harder to read, and harder to write as well. We can and should do better than C.

> And in that case, why not lift them into a language type system?

Easier said than done. First, lifting a new verification property into a type system requires changing the language or creating a new one, so it doesn't solve the problem (another rewrite?). Second, and more fundamentally, some properties cannot always be proven one way or another, but only admit sound classification as yes/no/maybe. Type systems don't usually work well with such properties. There's also the problem of how much of the specification power you want to include in the programming language. More on that below.

> it's very useful if all the tools share a common understanding of those properties.

Sure, but see my response to fpoling.

> it will have to be via a commonly understood specification that's a de facto language definition.

Some such standard or nearly-standard specification languages exist, e.g. JML for Java, and ACSL[1] (inspired JML and supported by frama-C) for C.

> So given we're creating a new safe language

Your new programming language can be whatever you like -- like Rust. The specification language -- for your new or legacy code -- can be rather orthogonal. Even Rust would require a formal specification language for greater correctness, as the language itself cannot specify many interesting properties. Whether, in terms of language design, it's better to unify the specification language and the programming language (as, say, Idris aims to do) or keep them separate is subject to a heated debate (dating all the way back to Dijkstra and Milner). Obviously, if the specification could be unified with the language without it having any negative effect, then that's something desirable; the problem is that many people believe that no such language (or even an idea for one) has been conceived of just yet.

> Even if it were as safe as Rust, C would still be harder to read, and harder to write as well. We can and should do better than C.

Oh, absolutely! I'm all in favor of using Rust over C! But that doesn't mean that rewriting existing code in C is worthwhile in terms of cost-benefit, if your goal is to increase correctness.

[1]: http://frama-c.com/acsl.html

> First, lifting a new verification property into a type system requires changing the language or creating a new one, so it doesn't solve the problem (another rewrite?).

Much of the value in using type systems is that, precisely because they're limited, they force you to write programs whose proofs of correctness would be simpler than if you didn't follow a type discipline. This is true even if you use an external logic for reasoning about your program.

In a language like Rust, I can often arrange things so that the burden of verification is split between type checking and simple high-school algebra calculations. What do I get in C? Gigantic yet intricate state spaces, which need to be split into subsets either manually or mechanically using who knows what heuristics. These subsets are in turn described by formulas containing lots of nested quantification, which is a lot more difficult for humans to deal with than just algebra.

> Second, and more fundamentally, some properties cannot always be proven one way or another, but only admit sound classification as yes/no/maybe. Type systems don't usually work well with such properties.

Type systems err on the side of safety: if no typing derivation can be constructed for your program, your program is wrong, even if your evaluation rules are untyped and your program wouldn't get stuck under them.

> Even Rust would require a formal specification language for greater correctness

This means nothing. Correctness is a binary question: your program is either right or wrong...

> as the language itself cannot specify many interesting properties.

... regardless of whether you've mechanically verified it or not.

> Whether, in terms of language design, it's better to unify the specification language and the programming language (as, say, Idris aims to do) or keep them separate is subject to a heated debate (dating all the way back to Dijkstra and Milner).

It's ultimately a matter of ergonomics, and there's a big continuum in between “prove everything internally” and “prove everything externally”. Rust sits very comfortably at some point in the middle.

My response to Imm was about something a little different from my original point, which is this: Rust is absolutely amazing; I love it! It is leaps and bounds better than C! Yet none of that makes rewriting every line of C out there in Rust the most cost-effective way of improving software quality.

> Yet none of that makes rewriting every line of C out there in Rust the most cost-effective way of improving software quality.

What I know not to be cost-effective in the long run is working around C's inability to enforce its own abstractions. Anything that makes abstractions easier to protect is an improvement over what we have now.

> working around C's inability to enforce its own abstractions

But you don't need to. We are talking about rewriting internal code that no one intends to touch, not about improving APIs.

> Anything that makes abstractions easier to protect is an improvement over what we have now.

Sure, so wrap C code with Rust. That's a whole other matter than rewriting it.

> But you don't need to. We are talking about rewriting internal code that no one intends to touch, not about improving APIs.

But it has to be touched, because it contains mistakes!

> Sure, so wrap C code with Rust. That's a whole other matter than rewriting it.

Reimplementing things in Rust from scratch has an important advantage: abstractions can be redesigned to maximize the extent to which the contract between API implementors and users is captured in types.

> But it has to be touched, because it contains mistakes!

Sure, but where exactly? Is manual translation into another language the best bang-for-the-buck approach you know for finding bugs?

> Reimplementing things in Rust from scratch has an important advantage

Of course it does! But is it the most cost-effective way to improve vast amounts of legacy code that isn't under active development?

Just for the sake of argument, suppose some 10MLOC (which comprise a minuscule, nearly negligible, portion of all legacy C code) contain, say, 500 serious, dangerous bugs, 450 of them could be fixed in a Rust rewrite that would cost $10M, while, say, 400 of them could be fixed using C tools for the cost of, say $1M. Wouldn't it make much more sense not to do the rewrite for 10x the cost and 12% of added utility? Of course the situation could be much more in favor of Rust or in favor of C, but we don't know! Wouldn't it at least be far more responsible to use tools that would help us know where we stand for relatively little effort before we commit to one approach over the other?

> Just for the sake of argument, suppose some 10MLOC (which comprise a minuscule, nearly negligible, portion of all legacy C code) contain, say, 500 serious, dangerous bugs, 450 of them could be fixed in a Rust rewrite that would cost $10M, while, say, 400 of them could be fixed using C tools for the cost of, say $1M. Wouldn't it make much more sense not to do the rewrite for 10x the cost and 12% of added utility?

I don't think 12% is the right way to think about it. The difference between 100 bugs and 50 bugs is at least as big as the difference between 200 bugs and 100 bugs, probably bigger - at least in terms of how much it costs. Suppose you go for the C approach, but turns out you really do need to get down to 50 outstanding bugs - at that point how much is it going to cost to do that in C? Suppose a year later you need to get down to 25? I think it's very easy to end up in a sunk costs situation where at each step improving the existing codebase is cheaper than rewriting, but overall you end up spending far more.

Maybe we need to focus on migration paths. Maybe strategies like targeted rewrites of critical pieces can offer the same level of incrementalism as improving existing C code, but greater overall efficiency. Or maybe there's just no affordable way to salvage existing legacy codebases. IMO in the coming decades we're going to see attackers reach a level of sophistication where any bug in network-facing code is exploited; at that point more-or-less the only useful code will be (provably) bug-free code. I think the path from legacy C code to bug-free code that goes via rewrite-in-Rust-today is ultimately cheaper than the one that goes via use-tooling-to-improve-the-C-today.

> Is manual translation into another language the best bang-for-the-buck approach you know for finding bugs?

For finding a single bug, no. For finding bugs in bulk, yes (or rather, for reducing the bug rate below a certain threshold, if that required threshold is low enough). I honestly think the costs of translating between languages are very much overestimated - it's much more similar to refactoring code for clarity than it is to writing a program from scratch.

(It doesn't have to be manual - there's no reason you can't do a semi-automated translation in the same way you'd do a semi-automated correctness proof.)

> I think it's very easy to end up in a sunk costs situation where at each step improving the existing codebase is cheaper than rewriting, but overall you end up spending far more.

I don't understand this analysis. 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). If a codebase turns out to be broken beyond repair, by all means -- rewrite. But we have no reason to assume that's the case, so why make such a costly assumption?

> at that point more-or-less the only useful code will be (provably) bug-free code

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.

> For finding bugs in bulk, yes

I must say I'm surprised. With all the automated test-generations and new static analysis tools out there, the first thing you reach for is a manual translation?

> it's much more similar to refactoring code for clarity than it is to writing a program from scratch.

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

> It doesn't have to be manual - there's no reason you can't do a semi-automated translation in the same way you'd do a semi-automated correctness proof.

The main reason I can think of is that no such tool currently exists. If it did, it may significantly reduce the cost of translation and change the equation. I'd be very excited to have such a tool, and, in fact, I think creating one is a better investment than starting to manually rewrite old, largely untouched and largely correct code.

[1]: I'm giving a talk about this in July at Curry On: http://curry-on.org/2016/sessions/why-writing-correct-softwa...

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

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

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.

> I think we're never going to be able to (affordably) prove (general) C code correct.

We are likely to never be able to affordably prove code in any language correct. The math is stacked strongly against us. The verification community works to make some specific properties of some kinds of programs affordable to verify; that's pretty much the best we hope for (and I think that's plenty).

> Yes. I think translation should be the first resort, because it obviates all the other approaches... and because better code makes subsequent analysis easier.

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

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

My recollection of current verification efforts is that the kind of code that's insanely difficult to port is exactly the same kind of code that's basically impossible to verify. People playing games with type punning (technically illegal), or worse yet, stuffing a few bits into pointers or stuffing pointers into doubles are surprisingly common (for efficiency reasons), and that's not going to fly with most verifiers.

It's not clear that building verifiers capable of handling the complex C code is any easier than mass rewriting into Rust (or other safe languages), nor that rewriting into more safely-analyzable subsets of C is easier (/more tenable) than into Rust.

First, a rewrite is costly even for simple code, where verification is easier. I don't know what percentage of code that is, but I'd assume not too small.

But even if simple, non-tricky code is the exception, is a rewrite (or verification) really worth it? Maybe in some cases it is, but you'd need to carefully analyze where. A "mass rewrite" is almost always a wasted effort, that would be best put to use elsewhere. Even in writing better tests.

The question is what value do you get from a rewrite. Nearly all post-C languages have strived for eliminating buffer overflows, which produce 80-90% of all security bugs. For string/buffer-laden libraries that get most of their input from the WWW, the value proposition to me seems very high.

Rust -- like any other non-research language -- achieves this particular feature mostly through runtime checks (which, I'd guess, are elided in many circumstances). If you're willing to pay for those, it's much easier to use a C compiler that adds them (and removes them if it can prove they're unnecessary, as I'm sure the Rust compiler does, too). Even adding some of those checks manually is likely a far smaller effort than rewriting everything.

Now, I'm not saying that if you just do that (and not use more powerful verification tools) the result would be as good as rewriting everything in Rust, but the difference would certainly not be worth the cost.

But my main point is this: if the industry decides to make a significant portion of mission-critical C code safer, we should do a careful cost/benefit analysis, and find the best approach to tackle each problem. I'm not saying that manually or automatically injecting overflow checks is what we should do, but I doubt that a wholesale rewrite in any language is the best way to achieve this goal. A complete rewrite of nearly endless code with uneven quality and very partial tests has never been, and likely never will be, a cost-effective or a very productive way of improving its quality (but write your new code in Rust!)

> Rust -- like any other non-research language -- achieves this particular feature mostly through runtime checks

This isn't true, and it's a big part of what makes rust interesting for this kind of work. There are array bounds checks, yes, but only with the indexing operator which is not idiomatic rust (FWIW, Rust has idiomatic iterators which allow LLVM to remove bounds checks at compile time). Nearly all of the other memory safety guarantees are from compile time checks.

It's fine for a general discussion about rewrites to be uninformed about the specifics of the target language, but citing incorrect specifics about a language isn't helping your case.

Yes, I know that, but we are talking about bounds checks! In many places where there is simple iteration, a C compiler would be able to prove no over/underflow, and where the pattern isn't so straightforward, a Rust rewrite would be even more expensive. Now, I don't know how many times I need to say it, but I have no doubts that Rust is "interesting for this kind of work". I absolutely fucking love Rust! I am just seriously questioning the economic sense of rewriting every piece of legacy code out there (billions of LOC!) whenever a new language comes along in an effort to improve its safety/correctness just because we know that there are probably lots of bugs in there somewhere. Draining the ocean with a spoon is guaranteed to find every piece of sunken treasure, but it's probably not the approach with the greatest bang-for-the-buck.

What would you say if in ten years people would say, "Ugh, Rust?! That hardly guarantees any interesting properties. Fine, it ensures there are no data races and dangling pointers, but does it make sure the library/program does what they're supposed to? Let's rewrite every line of code out there in Idris or ATS! That would be the best use of our time!" Whenever a library needs to be replaced -- either it doesn't serve modern requirements, it's hard to maintain and needs to undergo changes, or it is simply shown to be broken beyond repair, by all means -- write it in Rust! Gradually, there will be more and more Rust code out there, which is no doubt much better than C code. But a wholesale rewrite?

Bounds checks aren't really about underflow and overflow though? At least not as typically discussed. They're about determining whether the access to array contents is within the predefined region of memory which is covered by the array. And while Rust has bounds checked when directly indexing into an array, idiomatic Rust relies on iterators which have bounds checks that are nearly always removed by LLVM -- generally eliminating the runtime checks you referred to.

> I absolutely fucking love Rust!

Me too!

> I am just seriously questioning the economic sense of rewriting every piece of legacy code out there (billions of LOC!) whenever a new language comes along in an effort to improve its safety/correctness just because we know that there are probably lots of bugs in there somewhere.

Me too!

I don't know anyone who is seriously advocating for "rewrite literally everything in Rust." I use that expression to describe those who specifically call out OpenSSL, glibc, etc. every time a new CVE comes up which requires a fire drill. Rewriting critical infrastructure is very different from "everything," and even then, I've not made any assertion that we should do so. 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.

> What would you say if in ten years people would say, "Ugh, Rust?! That hardly guarantees any interesting properties.

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. If Rust is displaced by a language with better or more interesting safety properties, I will be elated (at least in part because to be displaced, Rust will have to have done OK in the meantime ;) ). But for now, I think it's worth finding out what mileage we can get out of Rust and its various properties and guarantees.

> Whenever a library needs to be replaced -- either it doesn't serve modern requirements, it's hard to maintain and needs to undergo changes, or it is simply shown to be broken beyond repair, by all means -- write it in Rust! Gradually, there will be more and more Rust code out there, which is no doubt much better than C code. But a wholesale rewrite?

So reading over your various responses, I think we're actually in general agreement. Any major change in a project requires careful risk assessment/management and justification. 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).

> Bounds checks aren't really about underflow and overflow though?

Buffer overflow, is possibly what is being referred to? That's definitely the province of bounds checking.

I don't know anyone who is seriously advocating for "rewrite literally everything in Rust."

Personally, I assumed that was supposed to mean "some critical subset of infrastructure". I'm not sure why pron settled on the particular interpretation they did (everything in the literal sense), but they've been careful to define that over and over in their comments, and very few have bothered to clarify like you have. It's almost enough to make me wonder a bit if the interpretation you and I have is actually the minority and a sizable portion of the rust community, or at least those involved here, actually want it in a literal sense, but I think that would be silly...

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

Awesome! Carefully collect data! We need it.

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

> Rust [...] achieves this particular feature mostly through runtime checks

If you do a 1:1 translation then sure. But idiomatic rust probably uses zero-overhead (or very nearly so, I haven't checked in a while) iterators and other higher level constructs that generate extremely efficient code and don't require bounds checks.

You won't see nearly as many "for (size_t i = 0; i < BOUND; i++) { ... array[i] ...}" in Rust, which means even though array bounds checking might be no faster in Rust, the fact that you don't use it as often is a big win.

The C language is sufficiently broken that's it really hard to reliably retrofit any type of safety features on top of it. Since people assume that C is portable assembler, they expect it to map very closely to the underlying machine, which makes even specification-permissible changes effectively impossible (good luck getting fat pointers or non-wraparound integer overflow working on real programs!).

The state of the art here for retrofitting C code is ASAN and tools like SoftBound, SAFECode, and baggy bounds, all of which use shadow memory techniques and impose about 100% overhead. And you can't use them simultaneously because there's a conflict on the shadow memory, which makes actually deploying software with security checks enabled impractical if not impossible.

Disclaimer: I've worked on research projects for automatically adding software protections to C/C++ code (albeit for integer overflows, not memory safety).

Once again: we are not talking about the brokenness of C, but about whether rewriting billions of lines of legacy code whenever a safer language comes along because surely it contains bugs is the most economically sensible way to improve software quality.

I am not talking about providing all the benefits a rewrite would, but I am suggesting something that would be orders of magnitude less expensive, and still very effective (and may actually have some benefits that a rewrite won't), with the net result of being an overall more effective strategy (and I am not talking about runtime tools but about whitebox fuzzing, concolic testing and static analysis tools).

>A far more feasible approach (though still very expensive) -- and probably a more "correct" one, even theoretically -- is to verify existing C code using some of the many excellent verification tools (from static analysis to white-box fuzzing and concolic testing) that exist for C

When I tried to verify C code (with hoare calculus, by hand) I found that rewriting that code in haskell and proving that to be correct was much easier. As a result i hardly know anything about the complexity of that code, but for me knowing it produces correct results was enough.

> When I tried to verify C code (with hoare calculus, by hand)

That's not the kind of verification I mean (proof of correctness, let alone deductive proof), but rather automated verification of "internal" program properties (aliasing, dangling pointers etc.), similar to those that could be achieved with type systems like those of Rust or Haskell. However, those tools could also prove stronger properties, probably with a bit more effort.

BTW, if you want to fully formally verify the correctness of C code, you don't need to do it by hand. There are tools that can help you (like Why[1] and various source-level model checkers).

[1]: http://why3.lri.fr/

Easy interaction with other languages is a double-edged sword. Too much of foreign calls may lead to unmaintainable code when knowledge of both languages and their libraries is required to even understand what is going on. And of cause, it makes it even harder to use a whole-program static verification as the tool now must understand both languages.

True, but this downside is still orders of magnitude less costly than rewriting "all" widely used C code out there. This is good as a limited exercise to learn the strengths and limitation of a new language, but as a serious undertaking a gross misuse of resources. Besides, by the time it's done, there will be a new language out there, with the same downside you point out. To avoid it, the software industry would basically do nothing but rewrite legacy code over and over.

"No so easy to use" does not mean no re-use. For this reason I really like how Elm interacts with JavaScript. The language requires to define so-called ports that provide explicit bindings to-from JS world. Thus it is not worth the efforts to call into JS function that does some trivial stuff. But interacting with bigger libraries is straightforward. As a big bonus guarantees of Elm's type system survive interaction with those libraries (unless the JS code in those libraries is malicious), so one does no need to know the details of those libraries to reason about Elm code.

Note that from this point of view rewriting C runtime library in Rust is not good as it creates too tight coupling between C and Rust worlds, requiring to write in a rather unnatural style in Rust. Besides, a lot of Musl essentially translates C calls into kernel ones when Rust typesystem brings no advantages.

> A far more feasible approach (though still very expensive) -- and probably a more "correct" one, even theoretically -- is to verify existing C code using some of the many excellent verification tools (from static analysis to white-box fuzzing and concolic testing) that exist for C[1].

Most static analysis tools for C suck:

(0) Few of them are actually sound. An unsound tool is basically worthless if you really want to be sure that your code has no errors.

(1) They suffer from modularity issues. As you say, they rely on analysis of the control flow of the program (abstract interpretation), which means that, more often than not, the different parts of your program end up related by monstrous preconditions and invariants that expose more implementation details than any sensible programmer would like.

(2) Finally, from a purely pragmatic point of view, they impose the burden of “jumping” between more levels of abstraction: C's syntax (which is already two-layered, thanks to the C preprocessor), some hopefully correct formal semantics for C, and whatever concepts (e.g., sets of states characterized by an invariant) that formal semantics is defined in terms of.

With type systems:

(0) We have a methodology (due to Wright and Felleisen) for proving that a language is type safe.

(1) The type system's intrinsic complexity establishes an upper bound on how intricate the interfaces between modules can be.

(2) For the most part, the programming only needs to care about the denotation of syntax in terms very close to the problem domain. The actual boring syntax processing is the type checker's job.

> It is more "correct" because, while perhaps not providing some of the other benefits, those tools can prove more properties than the Rust type system can, and such tools don't (yet) exist for Rust.

Using a single formal system to prove absolutely everything is impractical. Some things are more convenient to enforce mechanically and internally:

(0) Case analysis exhaustiveness: Humans are comically bad at this. OTOH, it's very easy for a type checker to make sure that a pattern matching block has an arm for every constructor of an algebraic data type.

(1) Separation of concerns: Parametric type abstraction guarantees that abstraction clients aren't exposed to the implementor's design choices.

While other things are easier to prove manually and externally:

(0) Equational laws: Not all algebraic theories are decidable, which means that there's no single search procedure that can decide whether a given equation (with all free variables implicitly universally quantified at the beginning) follows from others.

(1) Routine invariants that are obvious by inspection, and would be too burdensome to annotate in the syntax of a program.

I strongly agree with some of the things you say and strongly disagree with others, but we're not here to discuss the relative merits of static analysis (I'm not talking about deductively proving correctness) vs. type systems. We're talking about the relative merits of rewriting each one of the billions of lines of C code out there in Rust vs. using verification tools, in order to increase our confidence in the safety of the code. The argument isn't even about the quality of the result but the cost/benefit of the approach.

> static analysis (I'm not talking about deductively proving correctness)

What else could be the point to static analysis, if not completely ruling out bugs?

> vs. type systems.

Type-checking is a static analysis.

> We're talking about the relative merits of rewriting every line of C code out there in Rust vs. using verification tools,

Where exactly is the merit in deliberately choosing a more complicated approach to ruling out bugs?

> in order to increase our confidence in the safety of the code.

The conceptually simpler the approach, the more confidence one can have in the result.

> The argument isn't even about the quality of the result but the cost/benefit of the approach.

It's precisely in systems software where the cost of bugs is higher than everywhere else. Anything (types or otherwise) that simplifies the reasoning by which bugs can be ruled out in systems software is a strict improvement on the state of the art.

I don't think this is the place to debate verification theory and practice in general (I will be giving a talk about some aspects of the theory of software verification -- those that I've studied, at least -- at the upcoming Curry On conference in July, though not on the programming/spec language debate -- that is more religion than science; if you're interested, I would gladly debate various aspects of software correctness with you there; I think there’s a lot we disagree on). Here I'm talking about something else altogether.

Reply on news.ycombinator.com