> I can have cyclic graphs with mutable data without writing any unsafe code You can, because the libraries that you use fallback to unsafe blocks. How about t

> I can have cyclic graphs with mutable data without writing any unsafe code You can, because the libraries that you use fallback to unsafe blocks. How about those who want to write these libraries without having to use unsafe? > You will likely argue that using unsafe code in a library is just as bad as writing unsafe code, even if that library is used and tested by a lot of people and the unsafety is corralled behind a safe API. You would be wrong. just because you think I'd be wrong doesn't prove me being wrong. Why should I rely on unsafe if I can implement the same algorithms and data structures with proper safety guarantees, but not in Rust? Why should I stick to Rust specifically for that matter? > My current project is 170K lines of Rust code, and has 225 uses of unsafe. That's about 1.3 uses of 'unsafe' per 1000 lines of code. If I could write C++ code and introduce less than 2 exploitable vulnerabilities per 1000 lines of code I'd have an even higher opinion of myself than I already do. yeah, it shows your personal commitment to Rust toolchain. This is good. But what if you've already acquired some knowledge of more powerful tooling out there, and you're given a task to estimate applicability of these two toolchains to the development of Linux Kernel? > We should adopt proof systems that let us verify safety properties for those little bits of unsafe Rust code. We should not, however, make that a precondition for writing that vast majority of code that can be written in safe Rust in safe Rust. Why shouldn't we do it specifically for Linux Kernel? Why shouldn't we use compile-time checks for element incusion, length-based non-emptiness of containers instead of implementing another set of runtime validators? > Safe Rust is a sweet spot where the compiler and tools can verify a strong set of safety properties without the developer having to deal with proof systems and dependent types How do you define a sweet spot? Is it indeed a sweet spot when it comes to kernel development? Why does this spot happen to be at the level of Rust type system, and not somewhere else? > Trying to put the brakes on Rust and get everyone to buy into ATS instead is putting the needs of the few over the needs of the many. I'm actually arguing here from a position of technical merit of two tools in the context of Linux Kernel development, but for some reason you bring vague and non-technical definitions of "sweet spot", "lots of people using something", "needs of the few vs needs of many", which I've not mentioned anywhere in the thread.