10 ms·

I won't get tired of repeating the same comment in every topic that suggests Rust to be a great replacement of C in existing projects, that it isn't. The safet

I won't get tired of repeating the same comment in every topic that suggests Rust to be a great replacement of C in existing projects, that it isn't. The safety guarantees that Rust provides are neither unique nor complete, and if we discuss the amount of effort necessary for bringing new interfaces like the one this article mentions ("one can define a kmalloc_for_rust() symbol containing an un-inlined version"), we should compare it to other existing solutions, like ATS [1], that are designed to be seamlessly interoperable with C codebases without giving up on the safety side of the argument. Just a week ago there was a link in ATS reddit channel that advertised ATS Linux [2][3] initiative, that may be of great interest for the same people who are interested in bringing more memory sefety to Kernel development, without giving up on existing C interfaces and the toolchain[4]. [1] http://www.ats-lang.org/Documents.html#INT2PROGINATS http://www.ats-lang.org/Documents.html#INT2PROGINATS [2] https://www.reddit.com/r/ATS/comments/ibyczp/ats_linux/ https://www.reddit.com/r/ATS/comments/ibyczp/ats_linux/ [3] http://git.bejocama.org http://git.bejocama.org [4] http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/c2016.html http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/...

gpm 6y ago
Your evidence (that there are potentially other alternatives) doesn't support your claim (that Rust isn't a great C replacement). There can be multiple great C replacements. Not being "perfect" in terms of the guarantees you provide doesn't mean you aren't a great improvement. Nor would not providing any guarantees at all mean that a language is necessarily not a great improvement. That said, I would be very interested in seeing a comparison between C, Rust, and ATS in practical code. This is the first I'm hearing of ATS and it sounds interesting.
- ghostwriter 6y ago
  > Your evidence (that there are potentially other alternatives) doesn't support your claim (that Rust isn't a great C replacement). I didn't claim that Rust isn't a great replacement overall, I was specifically mentioning that it's not great for existing C codebases, by the fact that it requires significant work to replace internal interfaces that may be important for performance-, backward-compatibility- and conventional tooling reasons. It doesn't interoperate with C as well as other alternatives are capable of, whilst not being objectively better at safety guarantees either.
  - johncolanduoni 6y ago
    How does ATS provide safety guarantees without additional semantic information about the C code it’s linking to? If it does require that, then you’re in the same boat as Rust: your choices are trivial interoperation with no safety at the interfaces or encoding the semantics of the C interface in the new language. The only difference I can think of is built in ability to inline C from headers (based on your comment about kmalloc), is that the case for ATS?
    - ghostwriter 6y ago
      It's not only inclusion of the headers. ATS compiles to C, and it can inline C without FFI. The benefit that you receive is the ability to introduce gradual automated proofs around unchanged stable interfaces that are known to be safe. You start with inlining everything but the small core that is proven to be safe. Then you can iterate indefinitely at the desired pace to bring new layers of formally verified API in places of previously unverified C calls without breaking backward compatibility and expected runtime profiles (safe pointer-based memory access [1] and stack-allocated closures [2] as an example) [1] http://www.ats-lang.org/MYDATA/SPPSV-padl05.pdf http://www.ats-lang.org/MYDATA/SPPSV-padl05.pdf [2] http://ats-lang.github.io/DOCUMENT/ATS2TUTORIAL/HTML/c1267.html http://ats-lang.github.io/DOCUMENT/ATS2TUTORIAL/HTML/c1267.h...
      - johncolanduoni 6y ago
        This may need fewer code changes (if the code in question is correct and the interfaces can possible be implemented in a safe way, that is) but it still requires developers to write proofs in a dependent type theory. I’ve only looked at ATS briefly, but I’m familiar with a lot of the other languages in the space (Idris, Fstar, etc.). Are ATS’s proof tactics drastically more productive/brief than those (F* in particular, which has great aliasing reasoning)? If not I think you’re radically overestimating the approachability of this route compared to Rust.
        fluffy87 6y ago
joshuawarner32 6y ago
I’m glad that there other efforts for memory-safety going on concurrently, and we as a software community should absolutely continue to invest in those. I also agree that rust is not suited for all circumstances that people try to use it in - but I would contend that the set of situations where rust is absolutely the right choice is non-empty. I say this as part of a ~20 person team, rewriting business-critical software in Rust, where most of the engineers I talk with are glad they’re writing rust.
- JoshTriplett 6y ago
  It's certainly not just about safety. It's about the combination of safety, expressiveness, productivity, and various other factors.
  - nullc 6y ago
    Can someone cite a peer reviewed study that supports the belief that rust increases safety or productivity in actual use?
    - shock 6y ago
      > rust increases safety or productivity in actual use? compared to what?
      - nullc 6y ago
        Anything well known and widely deployed would be interesting. C++11 would be an obvious comparable, but C would be relevant considering the thread.
- ghostwriter 6y ago
  > but I would contend that the set of situations where rust is absolutely the right choice is non-empty Maybe I should've highlighted it in my initial comment, because I definitely agree that this list is non-empty for Rust. I was mentioning specifically existing C codebases that are heavily used in production around the world (last time a similar topic was related to QUEMU project).
stmw 6y ago
ATS certainly looks interestinb, but it's an academic language (of which there are many) that most people probably haven't heard of... At some point, the momentum of a new programming language is just as important -- in practical terms -- as its formal attributes and qualities.
- rumanator 6y ago
  Your centering your criticism of ATS on popularity. Does an investment on PR trumps technical merit?
  - dbaupp 6y ago
    Popularity and momentum translate into (and are proxies for) important things like: library availability, long-term maintenance and support, more edge cases are explored (so less “research”, breaking new ground and bugs when going off the beaten track), tooling and even availability of teaching material like documentation and tutorials.
    - ghostwriter 6y ago
      In case of ATS, any C library can be treated as a "unsafe-marked" ATS library, so there's no problem with library support, the problem is with their formal verification. And Rust libraries regularly suffer from the same lack of formally-verified and proven-to-be-safe APIs.
      - dbaupp 6y ago
        That helps with the "library availability" sub-point specifically, yes. However, there's a more than that when evaluating a language, as suggested by my comment above. In any case, if one is discussing modern and safe languages, there's a dramatic difference between using a C library and using a library native to the language. Even ignoring safety, the ergonomics/developer experience is dramatically different and the impedance mismatch can be very frustrating (for a "best case" example of this, Swift puts a lot of effort into exposing Objective-C interfaces as "swiftier" APIs automatically, but this benefits significantly from a relatively opinionated set of idioms in the source language, something arbitrary C libraries do not have). You're right that being able to import a C library directly is a very nice feature. > And Rust libraries regularly suffer from the same lack of formally-verified and proven-to-be-safe APIs. Right... but having a larger community means there's a much higher chance of a safe or easier-to-use library existing for any particular task. In particular, I think it means there's almost certainly more libraries in total, with more safe libraries and more unsafe libraries overall, so simply comparing number (or proportion) of low-safety libraries is misleading. (Formally verified is shifting the goal posts here: the bar is just "has a native library".)
kbenson 6y ago
> I won't get tired of repeating the same comment in every topic that suggests Rust to be a great replacement of C in existing projects, that it isn't. That's not what this is about, so even though you aren't tired of posting this, I'm not sure it's warranted. This is about the kernel supporting other languages in select places where it makes sense, such as kernel modules, where there's already an API in place to conform to. It's also not limited to Rust, it's about providing support for multiple other languages that could be beneficial in those locations. > I won't get tired of repeating the same comment in every topic that suggests Rust to be a great replacement of C in existing projects, that it isn't. Nobody is giving up on existing C interfaces. They are simply making sure those interfaces are not actively hostile to languages that aren't C by nature of how they are implemented in C. To be clear, the "kmalloc_for_rust" was mentioned as one possible way forward. Another would be a more advanced Rust bindgen tool that can determine how to deal with it automatically. Neither affect ATS, based on your description (although a "kmalloc_for_extern" might generally help any non-C language, which would probably be beneficial). If ATS doesn't require any changes to C to interoperate with it, this whole announcement should have zero impact on ATS, other than possibly making it easier to get an ATS module in-kernel since they're trying to make it easier in general for non-C modules. You can treat this as a zero-sum gain, where Rust or Go's gain is ATS' loss, in which case you might as well pack up your bags now, since the writing is on the wall based on publicity, or you can treat it as a rising tide raises all boats type situation, where more general acceptance of alternatives to C is still beneficial to ATS actually being allowed in-kernel, even if it doesn't play exactly to ATS' strengths. I know which one I would put my money behind as being a better strategy in the end.
- ghostwriter 6y ago
  > It's also not limited to Rust, it's about providing support for multiple other languages that could be beneficial in those locations But what are these benefits that other languages bring on the table? From the article it appears that proponents of the new toolchain mention memory-safety as the primary concern: > They focused on security concerns, citing work showing that around two-thirds of the kernel vulnerabilities that were assigned CVEs in both Android and Ubuntu stem from memory-safety issues. Rust, in principle, can completely avoid this error class via safer APIs enabled by its type system and borrow checker. So the natural follow-up question to that concern, it seems to me, would be whether there's something in the existing C/GCC toolchain (or around it) that can resolve the raised concerns without adopting a whole new toolchain (Rust/LLVM) and without having to extend the existing interface with language-specific suffixes like "kmalloc_for_rust".
ekidd 6y ago
Yes, I've seen this comment a number of times now. ATS is a very interesting language! But there are a wide range of options for formal verification of systems programs, including the techniques used for the formally verified seL4 kernel, ATS, recent Ada work, TLA+, etc. Some of these tools have been very successful for certain projects. But the more powerful proof systems involve tradeoffs. Frequently, you need to invest significant amounts of developer effort in exchange for very rigorously proven code. I've played with a number of these systems over the years, and they're great. But the costs would be hard to justify for many projects. Rust occupies a slightly different niche. It focuses on preventing several classes of memory errors and data races. It's certainly harder to learn than Python, but probably easier than some common subsets of C++. So the right tool for the job depends on what you're trying to do. If you want to formally verify your kernel's security model, or your distributed protocol, Rust would be a poor choice. If you want a language that makes it easy to work within sight of the metal, and that takes pains to make expensive operations visible, Rust can be a reasonable choice.
- deleted 6y ago
  [deleted]
- ghostwriter 6y ago
  I agree with your comment, and I think we are mentioning the same question here, that is essential for the kind of discussion that this article raises - whether or not a suggested amount of effort to bring Rust into existing and well-established C codebase is a great idea and is justified on a technical merit basis, compared to the effort of brining more sophisticated formal proof assistants that aim at non-intrusive interfacing with C while being productive for the cause of promoting safe and formally-verified programming. Python's gradual typing with MyPy demonstrated a great utility of static type checking that could be brought to existing project through many small and non-desruptive iterations. From my observation an learning of ATS, I expect even greater utility of gradual formal proofs that ATS enables for C. There are tons of successful C codebases, they are used in production around the world and contain a great amount of battle-tested knowledge. They just miss formal proofs that now could be gradually written for them.
gameswithgo 6y ago
>The safety guarantees that Rust provides are neither unique nor complete, Well no language can ever have "complete" safety guarantees. But I would like to know what other languages offer the same set of guarantees without GC overhead. This would include: * the usual memory safety * no nulls * no undefined behavior * no data races Does ATS guarantee those things?
- Athas 6y ago
  Yes, ATS can guarantee all those things and more. In particular, ATS allows you to write "unsafe" code, which you then prove safe with a mechanically verified proof. This is in contrast to unsafe Rust, which depends on programmer discipline, and has no (intra-language) mechanism for verification beyond the basic type system. You could say that Rust is all-or-nothing, while ATS allows gradual verification, as well as proving safe much more complex code than you can in Rust. I'm not going to claim that ATS is overall better than Rust - it's not - but it's a far more powerful language than Rust for safe systems programming. It's just that most people are not willing or able to pay the very high price in ergonomics. I recommend watching this presentation for a good idea of what ATS programming is like: https://www.youtube.com/watch?v=zt0OQb1DBko https://www.youtube.com/watch?v=zt0OQb1DBko In short, it's about as user-friendly as an overheating nuclear reactor.
  - ghostwriter 6y ago
    > It's just that most people are not willing or able to pay the very high price in ergonomics. Hopefully it will get better in ATS3 - https://github.com/githwxi/ATS-Xanadu#project-description https://github.com/githwxi/ATS-Xanadu#project-description
- deleted 6y ago
  [deleted]
- amelius 6y ago
  The problem is that Rust still keeps you thinking about memory management. From a security-perspective this makes it worse than GC'd languages.
scythe 6y ago
> I won't get tired of repeating the same comment in every topic that suggests Rust [...] we should compare it to other existing solutions, like ATS [1] One of the problems with repeating comments is that the previous replies are not incorporated into the discussion; for example, mine: >Back when it was on the PL shootout, ATS was consistently in the top five for performance. However, it was also consistently the worst in program size I looked into learning ATS some years ago before Rust existed, and shied away due to the complexity. It's been around much longer than Rust, and I think there's a reason it hasn't caught on: it's just too onerous. ATS might be appropriate for formally verified systems, but language ergonomics does matter, especially for a project with as many contributors as the Linux kernel.
outworlder 6y ago
> The safety guarantees that Rust provides are neither unique nor complete That sounds like "LEDs shouldn't be used for traffic lights because they don't melt snow", while ignoring all the benefits. Just add a heater where it is required. Rust does add benefits. Are these worth the extra effort? It seems that some people think it's worth it.
- ghostwriter 6y ago
  The question is more specific - does it add more benefit to the existing well-established C codebases, compared to other tooling particularly aiming at helping existing C codebases.
geofft 6y ago
As one of the presenters of this session, I'd like to reply by saying, this is cool! I'm hopeful it shows some good results! I'm not wedded to Rust in particular - it just seems to have the right balance of solving the particular problems the kernel wants to solve (there are plenty of other great languages like Go and Java and Python and Haskell and C++ that aren't suitable), easy to learn for people who have been working with C and have picked up an intuition for things like lifetimes and ownership that matter in C but aren't concrete, and popular (which is important because it means there are good learning resources, communities building things, etc.). It looks like the "ATS Linux" work is happening on a Git fork at http://git.bejocama.org/ats-linux-5.7.2 http://git.bejocama.org/ats-linux-5.7.2 . However, I don't see any commits there when I clone it - it looks like it's just the v5.7.2 tag from upstream. Do you know if there's any sample code that's been written demonstrating kernel code in ATS? I think that, empirically, we have built something that works. You can check it out (https://github.com/fishinabarrel/linux-kernel-module-rust https://github.com/fishinabarrel/linux-kernel-module-rust - see tests/* in particular). I'd be delighted to see folks who are excited about other languages build something in their language, too. I'd like to correct two specific things about your comment: > if we discuss the amount of effort necessary for bringing new interfaces like the one this article mentions ("one can define a kmalloc_for_rust() symbol containing an un-inlined version"), we should compare it to other existing solutions, like ATS Here is the amount of effort necessary to work around that: https://github.com/fishinabarrel/linux-kernel-module-rust/blob/master/src/allocator.rs#L11-L13 https://github.com/fishinabarrel/linux-kernel-module-rust/bl... I took a semester-long MIT class on a proof assistant (Coq) and I thought it was great but I'm still not fully comfortable with it. I realize that Coq and ATS are different languages, but I would humbly submit that if you compare the amount of effort spent calling krealloc instead of kmalloc vs. learning ATS, the former is probably lower. > without giving up on existing C interfaces and the toolchain Looking at Chapter 8 "Interaction with C" from the ATS book http://ats-lang.github.io/DOCUMENT/INT2PROGINATS/HTML/c2016.html http://ats-lang.github.io/DOCUMENT/INT2PROGINATS/HTML/c2016.... , it seems like ATS's interoperability with C is pretty comparable to Rust's https://doc.rust-lang.org/book/ch19-01-unsafe-rust.html#using-extern-functions-to-call-external-code https://doc.rust-lang.org/book/ch19-01-unsafe-rust.html#usin... - I don't think either of them require giving up on existing C interfaces or the C toolchain. One of the specific reasons to use Rust in this context instead of Go (which is a great language too) is that Rust is designed to fit in very closely with the C toolchain. The first paragraph of that chapter, which discusses how ATS's data structures can be zero-overhead bridged with C and you can view ATS as a better-typed frontend for C, seems to equally well apply to Rust. (In fact, as mentioned in the article, we'd love to automatically generate bindings from existing C interfaces. It turns out that most interfaces lack documentation - certainly machine-parseable docs, but often human-readable docs too - that indicates their ownership properties and locking constraints and so forth, but definitely the best approach is to get this sort of information into C annotations instead of having manual bindings in Rust. As a bonus, if it turns out that another language like ATS or Sing# or whatever is a better fit than Rust, the information is right there.)
Waterluvian 6y ago
It honestly doesn’t matter a whole lot what makes people excited about contributing to Linux. I think it’s worth embracing whatever does as long as it’s at worst harmless. Edit: I think what I’m trying to say is, let’s embrace what excites people.
simias 6y ago
The Linux kernel is fairly modular, I could definitely imagine rewriting subsystems by subsystems with fairly good ergonomics and safety. Like rewrite serial_core.c in Rust and then let people write serial drivers in Rust. Then the SPI code. Then the I2C. Then USB etc... Easier said than done of course, and definitely a huge effort especially for such a huge project as the Linux kernel, but there's also a significant amount of resources that could be allocated to that task by several large institutions. I don't know if it's a good idea, or if ATS or something else could be better, but I think you're overly pessimistic. Also "the safety guarantees that Rust provides are neither unique nor complete", while technically true, is also borderline FUD-y. At least you should expand on what you have in mind here, because I doubt that there exists a programing language that deals with low level hardware configuration that could ever provide "complete guarantees" about anything. And beyond that, keep in mind that Rust provides a lot more than just safety guarantees, its syntax is lot more advanced that good old C in particular for anything dealing with types (including destructuring, matching, inference etc...). Even if you don't get "full" safety right away it can still be a much nicer language to code in (and I say that as somebody who knows C well and quite like it overall).
- ghostwriter 6y ago
  > Also "the safety guarantees that Rust provides are neither unique nor complete", while technically true, is also borderline FUD-y. At least you should expand on what you have in mind here, because I doubt that there exists a programing language that deals with low level hardware configuration that could ever provide "complete guarantees" about anything. I meant inability to implement within the boundaries of safe Rust certain data structures and algorithms that ATS can prove to be safe. To name a few: stack-allocated closures, and safe pointer arithmetic programming [1]. For instance, ring buffers in Rust use "unsafe" and at some point there was a logical CVE in vec_deque that broke one invariant of the unsafe block [2]. Safe implementation of the ring buffer in ATS could be found in [1] [1] http://www.ats-lang.org/MYDATA/SPPSV-padl05.pdf http://www.ats-lang.org/MYDATA/SPPSV-padl05.pdf [2] https://gts3.org/2019/cve-2018-1000657.html https://gts3.org/2019/cve-2018-1000657.html
  - gpm 6y ago
Ericson2314 6y ago
To me the benefit of Rust is less safety, than better abstractions and modularity. Linux has been growing in complexity without much of a breaking point, and the discipline and separation of concerns high level languages could help with is a huge long-term benefit. (For example, say we could one day make a bunch of basic Linux drivers somewhat kernel agnostic? That would be amazing.) Now, ATS is I hear a fine language, but I think the ability to write good, and especially abstract, ATS is sadly too far outside of most kernel dev's skill set. Even among PL researchers, there is a tendency to write monolithic Coq---to wit, is there a Hackage or crates.io for Coq?---because abstraction are hard and the academic paper economy doesn't really reward it. Rust is just easy enough, and with enough crates.io momentum, that I hope the relative cost of reusable vs unreusable code will be less. And finally, it takes a lot of political will to introduce a new language in any existing project, let alone one as big and storied as Linux. Like it or not, but general popularity of the language absolutely does help with that.
darksaints 6y ago
Reading through your various replies to comments, it seems your argument boils down to the FFI issue, and I find that a little bizarre. Sure, ATS can inline library calls due to the lack of an FFI, and maybe it has a cleaner interface to those libraries, but now you've introduced a completely different set of problems: now you have to tell the compiler how to prove your code. In my experience, learning the fundamental concepts behind theorem proving is a lot harder of a problem than writing an FFI interface to a library. In fact, that problem is so easily solved that there are tools that do 99% of the work for you. And sure, maybe rust will never be able to inline C code, but inlining function calls is such a trivially small performance gap that most applications would never know the difference. I'm not convinced that there are better alternatives for contributing to or incrementally rewriting an existing code base. FFI is for most purposes a trivial impediment compared to the alternatives.
- ghostwriter 6y ago
  Hmm, I think my point is less about "native" FFI and more about safety guarantees and compatibility. Not every algorithm is portable to safe Rust without loosing on runtime/performance characteristics of the code, and falling back to unsafe Rust for that matter undermines the initial "rust is memory-safe" argument. C codebases are heavily invested in pointer-based algorithms and optimisations. ATS is able to verify them, Rust isn't.
stjohnswarts 6y ago
How do you know unless you try? I don't know why people are so against it. If you want to see vitriol see any discussion of rust on the now impotent slashdot community. If Linus is okay with it, I'm okay with it. He knows a lot more about the kernel than me and probably 99.99999% of of the people on the planet. I'm sure there are some awesome Einstein IQ people that know it even better than Linux, but I'll probably never meet them.
- hu3 6y ago
  > I don't know why people are so against it. There's an extremely high cost to introduce and maintain another language in a stack such as the Linux kernel. Everyone involved would be permanently impacted regardless of their opinion on the matter. It's not just a flag you can toggle. Otherwise Rust community would have already forked the Linux kernel instead of bugging their maintainers to RIIR. On top of that Rust compilation is very costly. It would render some devices that currently can compile the kernel unable to do so. Last I checked Rust fails to compile itself with 4GB of memory. Here's another user commenting about it: https://news.ycombinator.com/item?id=23059869 https://news.ycombinator.com/item?id=23059869
dang 6y ago
Please don't be repetitive in HN comments, though. Repetition is the enemy of curiosity and curiosity is the core value here. https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
- ghostwriter 6y ago
  What would be the proper way of informing those who are interested in the topic about available alternatives? I assume not everyone follows the same topics and there may be people who see the presented information and the relevant references for the first time.
  - pvg 6y ago
    You know the sort of person who comments 'Just install Linux' in every thread about more or less any kind of computer problem? You don't want to be that sort of person. If you're starting your comments with 'I'm not going to stop telling you to install Linux', it's probably a good time to check if you're not turning into the sort of person who's always telling you to install Linux.
    - ghostwriter 6y ago
      If I ommited that first part of the sentence the points made afterwards would remain the same. I did so to indicate that it's not the first time the Rust community suggests that something should be (re-)written in Rust for memory-safety reasons, in a project that has a well-established C-codebase. I'd argue it's the same "Just install Linux" situation that you mention, and that "Linux" may not be the answer.
      - pvg 6y ago
        it's not the first time the Rust community suggests that something should be (re-)written in Rust The article is not about that, though, it's specifically about the various issues surrounding the use of Rust for Linux kernel development.
      - 6y ago

gpm 6y ago

Your evidence (that there are potentially other alternatives) doesn't support your claim (that Rust isn't a great C replacement). There can be multiple great C replacements. Not being "perfect" in terms of the guarantees you provide doesn't mean you aren't a great improvement. Nor would not providing any guarantees at all mean that a language is necessarily not a great improvement. That said, I would be very interested in seeing a comparison between C, Rust, and ATS in practical code. This is the first I'm hearing of ATS and it sounds interesting.

ghostwriter 6y ago
> Your evidence (that there are potentially other alternatives) doesn't support your claim (that Rust isn't a great C replacement). I didn't claim that Rust isn't a great replacement overall, I was specifically mentioning that it's not great for existing C codebases, by the fact that it requires significant work to replace internal interfaces that may be important for performance-, backward-compatibility- and conventional tooling reasons. It doesn't interoperate with C as well as other alternatives are capable of, whilst not being objectively better at safety guarantees either.
- johncolanduoni 6y ago
  How does ATS provide safety guarantees without additional semantic information about the C code it’s linking to? If it does require that, then you’re in the same boat as Rust: your choices are trivial interoperation with no safety at the interfaces or encoding the semantics of the C interface in the new language. The only difference I can think of is built in ability to inline C from headers (based on your comment about kmalloc), is that the case for ATS?
  - ghostwriter 6y ago
    It's not only inclusion of the headers. ATS compiles to C, and it can inline C without FFI. The benefit that you receive is the ability to introduce gradual automated proofs around unchanged stable interfaces that are known to be safe. You start with inlining everything but the small core that is proven to be safe. Then you can iterate indefinitely at the desired pace to bring new layers of formally verified API in places of previously unverified C calls without breaking backward compatibility and expected runtime profiles (safe pointer-based memory access [1] and stack-allocated closures [2] as an example) [1] http://www.ats-lang.org/MYDATA/SPPSV-padl05.pdf http://www.ats-lang.org/MYDATA/SPPSV-padl05.pdf [2] http://ats-lang.github.io/DOCUMENT/ATS2TUTORIAL/HTML/c1267.html http://ats-lang.github.io/DOCUMENT/ATS2TUTORIAL/HTML/c1267.h...
    - johncolanduoni 6y ago
      This may need fewer code changes (if the code in question is correct and the interfaces can possible be implemented in a safe way, that is) but it still requires developers to write proofs in a dependent type theory. I’ve only looked at ATS briefly, but I’m familiar with a lot of the other languages in the space (Idris, Fstar, etc.). Are ATS’s proof tactics drastically more productive/brief than those (F* in particular, which has great aliasing reasoning)? If not I think you’re radically overestimating the approachability of this route compared to Rust.
      - fluffy87 6y ago

joshuawarner32 6y ago

I’m glad that there other efforts for memory-safety going on concurrently, and we as a software community should absolutely continue to invest in those. I also agree that rust is not suited for all circumstances that people try to use it in - but I would contend that the set of situations where rust is absolutely the right choice is non-empty. I say this as part of a ~20 person team, rewriting business-critical software in Rust, where most of the engineers I talk with are glad they’re writing rust.

JoshTriplett 6y ago
It's certainly not just about safety. It's about the combination of safety, expressiveness, productivity, and various other factors.
- nullc 6y ago
  Can someone cite a peer reviewed study that supports the belief that rust increases safety or productivity in actual use?
  - shock 6y ago
    > rust increases safety or productivity in actual use? compared to what?
    - nullc 6y ago
      Anything well known and widely deployed would be interesting. C++11 would be an obvious comparable, but C would be relevant considering the thread.
ghostwriter 6y ago
> but I would contend that the set of situations where rust is absolutely the right choice is non-empty Maybe I should've highlighted it in my initial comment, because I definitely agree that this list is non-empty for Rust. I was mentioning specifically existing C codebases that are heavily used in production around the world (last time a similar topic was related to QUEMU project).

stmw 6y ago

ATS certainly looks interestinb, but it's an academic language (of which there are many) that most people probably haven't heard of... At some point, the momentum of a new programming language is just as important -- in practical terms -- as its formal attributes and qualities.

rumanator 6y ago
Your centering your criticism of ATS on popularity. Does an investment on PR trumps technical merit?
- dbaupp 6y ago
  Popularity and momentum translate into (and are proxies for) important things like: library availability, long-term maintenance and support, more edge cases are explored (so less “research”, breaking new ground and bugs when going off the beaten track), tooling and even availability of teaching material like documentation and tutorials.
  - ghostwriter 6y ago
    In case of ATS, any C library can be treated as a "unsafe-marked" ATS library, so there's no problem with library support, the problem is with their formal verification. And Rust libraries regularly suffer from the same lack of formally-verified and proven-to-be-safe APIs.
    - dbaupp 6y ago
      That helps with the "library availability" sub-point specifically, yes. However, there's a more than that when evaluating a language, as suggested by my comment above. In any case, if one is discussing modern and safe languages, there's a dramatic difference between using a C library and using a library native to the language. Even ignoring safety, the ergonomics/developer experience is dramatically different and the impedance mismatch can be very frustrating (for a "best case" example of this, Swift puts a lot of effort into exposing Objective-C interfaces as "swiftier" APIs automatically, but this benefits significantly from a relatively opinionated set of idioms in the source language, something arbitrary C libraries do not have). You're right that being able to import a C library directly is a very nice feature. > And Rust libraries regularly suffer from the same lack of formally-verified and proven-to-be-safe APIs. Right... but having a larger community means there's a much higher chance of a safe or easier-to-use library existing for any particular task. In particular, I think it means there's almost certainly more libraries in total, with more safe libraries and more unsafe libraries overall, so simply comparing number (or proportion) of low-safety libraries is misleading. (Formally verified is shifting the goal posts here: the bar is just "has a native library".)

kbenson 6y ago

> I won't get tired of repeating the same comment in every topic that suggests Rust to be a great replacement of C in existing projects, that it isn't. That's not what this is about, so even though you aren't tired of posting this, I'm not sure it's warranted. This is about the kernel supporting other languages in select places where it makes sense, such as kernel modules, where there's already an API in place to conform to. It's also not limited to Rust, it's about providing support for multiple other languages that could be beneficial in those locations. > I won't get tired of repeating the same comment in every topic that suggests Rust to be a great replacement of C in existing projects, that it isn't. Nobody is giving up on existing C interfaces. They are simply making sure those interfaces are not actively hostile to languages that aren't C by nature of how they are implemented in C. To be clear, the "kmalloc_for_rust" was mentioned as one possible way forward. Another would be a more advanced Rust bindgen tool that can determine how to deal with it automatically. Neither affect ATS, based on your description (although a "kmalloc_for_extern" might generally help any non-C language, which would probably be beneficial). If ATS doesn't require any changes to C to interoperate with it, this whole announcement should have zero impact on ATS, other than possibly making it easier to get an ATS module in-kernel since they're trying to make it easier in general for non-C modules. You can treat this as a zero-sum gain, where Rust or Go's gain is ATS' loss, in which case you might as well pack up your bags now, since the writing is on the wall based on publicity, or you can treat it as a rising tide raises all boats type situation, where more general acceptance of alternatives to C is still beneficial to ATS actually being allowed in-kernel, even if it doesn't play exactly to ATS' strengths. I know which one I would put my money behind as being a better strategy in the end.

ghostwriter 6y ago
> It's also not limited to Rust, it's about providing support for multiple other languages that could be beneficial in those locations But what are these benefits that other languages bring on the table? From the article it appears that proponents of the new toolchain mention memory-safety as the primary concern: > They focused on security concerns, citing work showing that around two-thirds of the kernel vulnerabilities that were assigned CVEs in both Android and Ubuntu stem from memory-safety issues. Rust, in principle, can completely avoid this error class via safer APIs enabled by its type system and borrow checker. So the natural follow-up question to that concern, it seems to me, would be whether there's something in the existing C/GCC toolchain (or around it) that can resolve the raised concerns without adopting a whole new toolchain (Rust/LLVM) and without having to extend the existing interface with language-specific suffixes like "kmalloc_for_rust".

ekidd 6y ago

Yes, I've seen this comment a number of times now. ATS is a very interesting language! But there are a wide range of options for formal verification of systems programs, including the techniques used for the formally verified seL4 kernel, ATS, recent Ada work, TLA+, etc. Some of these tools have been very successful for certain projects. But the more powerful proof systems involve tradeoffs. Frequently, you need to invest significant amounts of developer effort in exchange for very rigorously proven code. I've played with a number of these systems over the years, and they're great. But the costs would be hard to justify for many projects. Rust occupies a slightly different niche. It focuses on preventing several classes of memory errors and data races. It's certainly harder to learn than Python, but probably easier than some common subsets of C++. So the right tool for the job depends on what you're trying to do. If you want to formally verify your kernel's security model, or your distributed protocol, Rust would be a poor choice. If you want a language that makes it easy to work within sight of the metal, and that takes pains to make expensive operations visible, Rust can be a reasonable choice.

deleted 6y ago
[deleted]
ghostwriter 6y ago
I agree with your comment, and I think we are mentioning the same question here, that is essential for the kind of discussion that this article raises - whether or not a suggested amount of effort to bring Rust into existing and well-established C codebase is a great idea and is justified on a technical merit basis, compared to the effort of brining more sophisticated formal proof assistants that aim at non-intrusive interfacing with C while being productive for the cause of promoting safe and formally-verified programming. Python's gradual typing with MyPy demonstrated a great utility of static type checking that could be brought to existing project through many small and non-desruptive iterations. From my observation an learning of ATS, I expect even greater utility of gradual formal proofs that ATS enables for C. There are tons of successful C codebases, they are used in production around the world and contain a great amount of battle-tested knowledge. They just miss formal proofs that now could be gradually written for them.

gameswithgo 6y ago

>The safety guarantees that Rust provides are neither unique nor complete, Well no language can ever have "complete" safety guarantees. But I would like to know what other languages offer the same set of guarantees without GC overhead. This would include: * the usual memory safety * no nulls * no undefined behavior * no data races Does ATS guarantee those things?

Athas 6y ago
Yes, ATS can guarantee all those things and more. In particular, ATS allows you to write "unsafe" code, which you then prove safe with a mechanically verified proof. This is in contrast to unsafe Rust, which depends on programmer discipline, and has no (intra-language) mechanism for verification beyond the basic type system. You could say that Rust is all-or-nothing, while ATS allows gradual verification, as well as proving safe much more complex code than you can in Rust. I'm not going to claim that ATS is overall better than Rust - it's not - but it's a far more powerful language than Rust for safe systems programming. It's just that most people are not willing or able to pay the very high price in ergonomics. I recommend watching this presentation for a good idea of what ATS programming is like: https://www.youtube.com/watch?v=zt0OQb1DBko https://www.youtube.com/watch?v=zt0OQb1DBko In short, it's about as user-friendly as an overheating nuclear reactor.
- ghostwriter 6y ago
  > It's just that most people are not willing or able to pay the very high price in ergonomics. Hopefully it will get better in ATS3 - https://github.com/githwxi/ATS-Xanadu#project-description https://github.com/githwxi/ATS-Xanadu#project-description
deleted 6y ago
[deleted]
amelius 6y ago
The problem is that Rust still keeps you thinking about memory management. From a security-perspective this makes it worse than GC'd languages.

scythe 6y ago

> I won't get tired of repeating the same comment in every topic that suggests Rust [...] we should compare it to other existing solutions, like ATS [1] One of the problems with repeating comments is that the previous replies are not incorporated into the discussion; for example, mine: >Back when it was on the PL shootout, ATS was consistently in the top five for performance. However, it was also consistently the worst in program size I looked into learning ATS some years ago before Rust existed, and shied away due to the complexity. It's been around much longer than Rust, and I think there's a reason it hasn't caught on: it's just too onerous. ATS might be appropriate for formally verified systems, but language ergonomics does matter, especially for a project with as many contributors as the Linux kernel.

outworlder 6y ago

> The safety guarantees that Rust provides are neither unique nor complete That sounds like "LEDs shouldn't be used for traffic lights because they don't melt snow", while ignoring all the benefits. Just add a heater where it is required. Rust does add benefits. Are these worth the extra effort? It seems that some people think it's worth it.

ghostwriter 6y ago
The question is more specific - does it add more benefit to the existing well-established C codebases, compared to other tooling particularly aiming at helping existing C codebases.

geofft 6y ago

As one of the presenters of this session, I'd like to reply by saying, this is cool! I'm hopeful it shows some good results! I'm not wedded to Rust in particular - it just seems to have the right balance of solving the particular problems the kernel wants to solve (there are plenty of other great languages like Go and Java and Python and Haskell and C++ that aren't suitable), easy to learn for people who have been working with C and have picked up an intuition for things like lifetimes and ownership that matter in C but aren't concrete, and popular (which is important because it means there are good learning resources, communities building things, etc.). It looks like the "ATS Linux" work is happening on a Git fork at http://git.bejocama.org/ats-linux-5.7.2 http://git.bejocama.org/ats-linux-5.7.2 . However, I don't see any commits there when I clone it - it looks like it's just the v5.7.2 tag from upstream. Do you know if there's any sample code that's been written demonstrating kernel code in ATS? I think that, empirically, we have built something that works. You can check it out (https://github.com/fishinabarrel/linux-kernel-module-rust https://github.com/fishinabarrel/linux-kernel-module-rust - see tests/* in particular). I'd be delighted to see folks who are excited about other languages build something in their language, too. I'd like to correct two specific things about your comment: > if we discuss the amount of effort necessary for bringing new interfaces like the one this article mentions ("one can define a kmalloc_for_rust() symbol containing an un-inlined version"), we should compare it to other existing solutions, like ATS Here is the amount of effort necessary to work around that: https://github.com/fishinabarrel/linux-kernel-module-rust/blob/master/src/allocator.rs#L11-L13 https://github.com/fishinabarrel/linux-kernel-module-rust/bl... I took a semester-long MIT class on a proof assistant (Coq) and I thought it was great but I'm still not fully comfortable with it. I realize that Coq and ATS are different languages, but I would humbly submit that if you compare the amount of effort spent calling krealloc instead of kmalloc vs. learning ATS, the former is probably lower. > without giving up on existing C interfaces and the toolchain Looking at Chapter 8 "Interaction with C" from the ATS book http://ats-lang.github.io/DOCUMENT/INT2PROGINATS/HTML/c2016.html http://ats-lang.github.io/DOCUMENT/INT2PROGINATS/HTML/c2016.... , it seems like ATS's interoperability with C is pretty comparable to Rust's https://doc.rust-lang.org/book/ch19-01-unsafe-rust.html#using-extern-functions-to-call-external-code https://doc.rust-lang.org/book/ch19-01-unsafe-rust.html#usin... - I don't think either of them require giving up on existing C interfaces or the C toolchain. One of the specific reasons to use Rust in this context instead of Go (which is a great language too) is that Rust is designed to fit in very closely with the C toolchain. The first paragraph of that chapter, which discusses how ATS's data structures can be zero-overhead bridged with C and you can view ATS as a better-typed frontend for C, seems to equally well apply to Rust. (In fact, as mentioned in the article, we'd love to automatically generate bindings from existing C interfaces. It turns out that most interfaces lack documentation - certainly machine-parseable docs, but often human-readable docs too - that indicates their ownership properties and locking constraints and so forth, but definitely the best approach is to get this sort of information into C annotations instead of having manual bindings in Rust. As a bonus, if it turns out that another language like ATS or Sing# or whatever is a better fit than Rust, the information is right there.)

Waterluvian 6y ago

It honestly doesn’t matter a whole lot what makes people excited about contributing to Linux. I think it’s worth embracing whatever does as long as it’s at worst harmless. Edit: I think what I’m trying to say is, let’s embrace what excites people.

simias 6y ago

The Linux kernel is fairly modular, I could definitely imagine rewriting subsystems by subsystems with fairly good ergonomics and safety. Like rewrite serial_core.c in Rust and then let people write serial drivers in Rust. Then the SPI code. Then the I2C. Then USB etc... Easier said than done of course, and definitely a huge effort especially for such a huge project as the Linux kernel, but there's also a significant amount of resources that could be allocated to that task by several large institutions. I don't know if it's a good idea, or if ATS or something else could be better, but I think you're overly pessimistic. Also "the safety guarantees that Rust provides are neither unique nor complete", while technically true, is also borderline FUD-y. At least you should expand on what you have in mind here, because I doubt that there exists a programing language that deals with low level hardware configuration that could ever provide "complete guarantees" about anything. And beyond that, keep in mind that Rust provides a lot more than just safety guarantees, its syntax is lot more advanced that good old C in particular for anything dealing with types (including destructuring, matching, inference etc...). Even if you don't get "full" safety right away it can still be a much nicer language to code in (and I say that as somebody who knows C well and quite like it overall).

ghostwriter 6y ago
> Also "the safety guarantees that Rust provides are neither unique nor complete", while technically true, is also borderline FUD-y. At least you should expand on what you have in mind here, because I doubt that there exists a programing language that deals with low level hardware configuration that could ever provide "complete guarantees" about anything. I meant inability to implement within the boundaries of safe Rust certain data structures and algorithms that ATS can prove to be safe. To name a few: stack-allocated closures, and safe pointer arithmetic programming [1]. For instance, ring buffers in Rust use "unsafe" and at some point there was a logical CVE in vec_deque that broke one invariant of the unsafe block [2]. Safe implementation of the ring buffer in ATS could be found in [1] [1] http://www.ats-lang.org/MYDATA/SPPSV-padl05.pdf http://www.ats-lang.org/MYDATA/SPPSV-padl05.pdf [2] https://gts3.org/2019/cve-2018-1000657.html https://gts3.org/2019/cve-2018-1000657.html
- gpm 6y ago

Ericson2314 6y ago

To me the benefit of Rust is less safety, than better abstractions and modularity. Linux has been growing in complexity without much of a breaking point, and the discipline and separation of concerns high level languages could help with is a huge long-term benefit. (For example, say we could one day make a bunch of basic Linux drivers somewhat kernel agnostic? That would be amazing.) Now, ATS is I hear a fine language, but I think the ability to write good, and especially abstract, ATS is sadly too far outside of most kernel dev's skill set. Even among PL researchers, there is a tendency to write monolithic Coq---to wit, is there a Hackage or crates.io for Coq?---because abstraction are hard and the academic paper economy doesn't really reward it. Rust is just easy enough, and with enough crates.io momentum, that I hope the relative cost of reusable vs unreusable code will be less. And finally, it takes a lot of political will to introduce a new language in any existing project, let alone one as big and storied as Linux. Like it or not, but general popularity of the language absolutely does help with that.

darksaints 6y ago

Reading through your various replies to comments, it seems your argument boils down to the FFI issue, and I find that a little bizarre. Sure, ATS can inline library calls due to the lack of an FFI, and maybe it has a cleaner interface to those libraries, but now you've introduced a completely different set of problems: now you have to tell the compiler how to prove your code. In my experience, learning the fundamental concepts behind theorem proving is a lot harder of a problem than writing an FFI interface to a library. In fact, that problem is so easily solved that there are tools that do 99% of the work for you. And sure, maybe rust will never be able to inline C code, but inlining function calls is such a trivially small performance gap that most applications would never know the difference. I'm not convinced that there are better alternatives for contributing to or incrementally rewriting an existing code base. FFI is for most purposes a trivial impediment compared to the alternatives.

ghostwriter 6y ago
Hmm, I think my point is less about "native" FFI and more about safety guarantees and compatibility. Not every algorithm is portable to safe Rust without loosing on runtime/performance characteristics of the code, and falling back to unsafe Rust for that matter undermines the initial "rust is memory-safe" argument. C codebases are heavily invested in pointer-based algorithms and optimisations. ATS is able to verify them, Rust isn't.

stjohnswarts 6y ago

How do you know unless you try? I don't know why people are so against it. If you want to see vitriol see any discussion of rust on the now impotent slashdot community. If Linus is okay with it, I'm okay with it. He knows a lot more about the kernel than me and probably 99.99999% of of the people on the planet. I'm sure there are some awesome Einstein IQ people that know it even better than Linux, but I'll probably never meet them.

hu3 6y ago
> I don't know why people are so against it. There's an extremely high cost to introduce and maintain another language in a stack such as the Linux kernel. Everyone involved would be permanently impacted regardless of their opinion on the matter. It's not just a flag you can toggle. Otherwise Rust community would have already forked the Linux kernel instead of bugging their maintainers to RIIR. On top of that Rust compilation is very costly. It would render some devices that currently can compile the kernel unable to do so. Last I checked Rust fails to compile itself with 4GB of memory. Here's another user commenting about it: https://news.ycombinator.com/item?id=23059869 https://news.ycombinator.com/item?id=23059869

dang 6y ago

Please don't be repetitive in HN comments, though. Repetition is the enemy of curiosity and curiosity is the core value here. https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html

ghostwriter 6y ago
What would be the proper way of informing those who are interested in the topic about available alternatives? I assume not everyone follows the same topics and there may be people who see the presented information and the relevant references for the first time.
- pvg 6y ago
  You know the sort of person who comments 'Just install Linux' in every thread about more or less any kind of computer problem? You don't want to be that sort of person. If you're starting your comments with 'I'm not going to stop telling you to install Linux', it's probably a good time to check if you're not turning into the sort of person who's always telling you to install Linux.
  - ghostwriter 6y ago
    If I ommited that first part of the sentence the points made afterwards would remain the same. I did so to indicate that it's not the first time the Rust community suggests that something should be (re-)written in Rust for memory-safety reasons, in a project that has a well-established C-codebase. I'd argue it's the same "Just install Linux" situation that you mention, and that "Linux" may not be the answer.
    - pvg 6y ago
      it's not the first time the Rust community suggests that something should be (re-)written in Rust The article is not about that, though, it's specifically about the various issues surrounding the use of Rust for Linux kernel development.
    - 6y ago