4 ms·

It's moving the goal posts and changing the point of the discussion. We can equally well say that that "Rust formally verifies your safe functions", and that th

by dbaupp 6y ago

It's moving the goal posts and changing the point of the discussion. We can equally well say that that "Rust formally verifies your safe functions", and that this reduces how much code review is required... it's a matter of degree and specifics. Focusing on pointer manipulations is also misleading: it's entirely true that it's dangerous, but most Rust code does not need to do any sort of raw pointer manipulation. For instance, there's extensive work on operating systems and other low level code that involves both inherent unsafety due to hardware specifics (that is, ATS almost certainly does not model it natively) and safe Rust wrappers (i.e. proofs of safety) for the unsafety at a surprisingly low level: - a recent series: https://www.ecorax.net/as-above-so-below-1/ https://www.ecorax.net/as-above-so-below-1/ https://www.ecorax.net/as-above-so-below-2/ https://www.ecorax.net/as-above-so-below-2/ - a long-standing operating system: https://os.phil-opp.com/ https://os.phil-opp.com/ Finally, if you are happy to cherry-pick specific examples, https://bluishcoder.co.nz/2017/02/22/borrowing-internal-pointers-in-ats.html https://bluishcoder.co.nz/2017/02/22/borrowing-internal-poin... discusses a case where Rust is able to prove more things safe than ATS 2 (at the time of writing). Plus... this is still ignoring all of the other factors why popularity and momentum are useful reasons to choose a language.

ghostwriter 6y ago
> We can equally well say that that "Rust formally verifies your safe functions", and that this reduces how much code review is required... it's a matter of degree and specifics. You cannot say that while this kind of CVE is possible https://gts3.org/2019/cve-2018-1000657.html https://gts3.org/2019/cve-2018-1000657.html and as long as Rust is not capable of performing safe pointer manipulations. The above issue may be solved for VecDeque in stdlib, but what about other data structures and algorithms in the wild? > Focusing on pointer manipulations is also misleading Remember that the discussion is happening in the topic about brining Rust into well-established C codebase, and C uses pointer-based arithmetics all the time, sometimes the whole algorithms are implemented this way because it brings efficiency to lower-level interfaces that are supposed to be very fast. If the motivation to bring a new tool is pronounced as "let's make it safe", why should we allow the argument to fallback into the "unsafe Rust" territory? > For instance, there's extensive work on operating systems and other low level code that involves both inherent unsafety due to hardware specifics I'm not going argue against that, because it's not related to the current topic related to Linux Kernel. > Finally, if you are happy to cherry-pick specific examples, https://bluishcoder.co.nz/2017/02/22/borrowing-internal-poin.. https://bluishcoder.co.nz/2017/02/22/borrowing-internal-poin.... discusses a case where Rust is able to prove more things safe than ATS 2 (at the time of writing). it's not more, it's one specific example. Shall we now enumerate all the things that both languages are able to prove? I think we should, to make it clear what the differences are and what is possible to prove safe. That's exactly my point about comparing brining Rust into existing C codebases with alternative tooling available specifically for C codebases.
- roca 6y ago
  "In the wild" one hardly ever has to write unsafe Rust data structures and algorithms. > If the motivation to bring a new tool is pronounced as "let's make it safe", why should we allow the argument to fallback into the "unsafe Rust" territory? Because going from 0% of code proven safe by the compiler to 99% is very valuable. Verifying the remaining code is desirable but not as valuable as what Rust already provides. Having said that, it would indeed be great to have a proof system for verifying properties of unsafe Rust code. Much work has been done in that area: https://alastairreid.github.io/rust-verification-tools/ https://alastairreid.github.io/rust-verification-tools/ Something to look forward to.
  - ghostwriter 6y ago
    > "In the wild" one hardly ever has to write unsafe Rust data structures and algorithms. one has to do it all the time if cyclic mutable graphs or specific buffers/caches are involved. > Verifying the remaining code is desirable but not as valuable as what Rust already provides. How do we know that? What are the criteria and the thresholds that lead us to that conclusion? Is it true for all fields where the language can be used? What should we do about inability to express more precise constraints at compile time? Shall we stop on Rust, or try to embrace more powerful tools that already support Dependent Types in low-level systems programming? These checks enable a whole new world of expressive powers and correctness guarantees, even compared to the cool borrow-checker. ATS supports them today [1] [1] http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/p2241.html http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/...
    - roca 6y ago
      I can have cyclic graphs with mutable data without writing any unsafe code: https://docs.rs/petgraph/0.5.1/petgraph/ https://docs.rs/petgraph/0.5.1/petgraph/ "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.

by dbaupp 6y ago

ghostwriter 6y ago

> We can equally well say that that "Rust formally verifies your safe functions", and that this reduces how much code review is required... it's a matter of degree and specifics. You cannot say that while this kind of CVE is possible https://gts3.org/2019/cve-2018-1000657.html https://gts3.org/2019/cve-2018-1000657.html and as long as Rust is not capable of performing safe pointer manipulations. The above issue may be solved for VecDeque in stdlib, but what about other data structures and algorithms in the wild? > Focusing on pointer manipulations is also misleading Remember that the discussion is happening in the topic about brining Rust into well-established C codebase, and C uses pointer-based arithmetics all the time, sometimes the whole algorithms are implemented this way because it brings efficiency to lower-level interfaces that are supposed to be very fast. If the motivation to bring a new tool is pronounced as "let's make it safe", why should we allow the argument to fallback into the "unsafe Rust" territory? > For instance, there's extensive work on operating systems and other low level code that involves both inherent unsafety due to hardware specifics I'm not going argue against that, because it's not related to the current topic related to Linux Kernel. > Finally, if you are happy to cherry-pick specific examples, https://bluishcoder.co.nz/2017/02/22/borrowing-internal-poin.. https://bluishcoder.co.nz/2017/02/22/borrowing-internal-poin.... discusses a case where Rust is able to prove more things safe than ATS 2 (at the time of writing). it's not more, it's one specific example. Shall we now enumerate all the things that both languages are able to prove? I think we should, to make it clear what the differences are and what is possible to prove safe. That's exactly my point about comparing brining Rust into existing C codebases with alternative tooling available specifically for C codebases.

roca 6y ago
"In the wild" one hardly ever has to write unsafe Rust data structures and algorithms. > If the motivation to bring a new tool is pronounced as "let's make it safe", why should we allow the argument to fallback into the "unsafe Rust" territory? Because going from 0% of code proven safe by the compiler to 99% is very valuable. Verifying the remaining code is desirable but not as valuable as what Rust already provides. Having said that, it would indeed be great to have a proof system for verifying properties of unsafe Rust code. Much work has been done in that area: https://alastairreid.github.io/rust-verification-tools/ https://alastairreid.github.io/rust-verification-tools/ Something to look forward to.
- ghostwriter 6y ago
  > "In the wild" one hardly ever has to write unsafe Rust data structures and algorithms. one has to do it all the time if cyclic mutable graphs or specific buffers/caches are involved. > Verifying the remaining code is desirable but not as valuable as what Rust already provides. How do we know that? What are the criteria and the thresholds that lead us to that conclusion? Is it true for all fields where the language can be used? What should we do about inability to express more precise constraints at compile time? Shall we stop on Rust, or try to embrace more powerful tools that already support Dependent Types in low-level systems programming? These checks enable a whole new world of expressive powers and correctness guarantees, even compared to the cool borrow-checker. ATS supports them today [1] [1] http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/p2241.html http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/...
  - roca 6y ago
    I can have cyclic graphs with mutable data without writing any unsafe code: https://docs.rs/petgraph/0.5.1/petgraph/ https://docs.rs/petgraph/0.5.1/petgraph/ "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.