"Specific buffers/caches" is ambiguous. For embedded systems there are crates that provide safe interfaces to memory-mapped hardware.
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.
> How do we know that? What are the criteria and the thresholds that lead us to that conclusion?
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.
> Is it true for all fields where the language can be used?
I'm sure we're both imaginative enough to dream up some "field" narrow enough to disprove any universally quantified proposition.
> What should we do about inability to express more precise constraints at compile time?
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.
> Shall we stop on Rust, or try to embrace more powerful tools that already support Dependent Types in low-level systems programming?
That is a false dichotomy.
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, with lots of engineering to produce helpful messages when things go wrong. Plus a large library ecosystem that, among other things, provides lots of safe abstractions over unsafe code. 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 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.
"Specific buffers/caches" is ambiguous. For embedded systems there are crates that provide safe interfaces to memory-mapped hardware.
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.
> How do we know that? What are the criteria and the thresholds that lead us to that conclusion?
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.
> Is it true for all fields where the language can be used?
I'm sure we're both imaginative enough to dream up some "field" narrow enough to disprove any universally quantified proposition.
> What should we do about inability to express more precise constraints at compile time?
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.
> Shall we stop on Rust, or try to embrace more powerful tools that already support Dependent Types in low-level systems programming?
That is a false dichotomy.
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, with lots of engineering to produce helpful messages when things go wrong. Plus a large library ecosystem that, among other things, provides lots of safe abstractions over unsafe code. 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.