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 particula

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