6 ms·

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

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

rumanator 6y ago
> 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. The dramatic nature of that difference is whether that library exists or not. Odds are, if exists then it's written in C. Thus this point is mute with regards to Rust because at best it's relegated to a nice-to-have, in the sense you can enjoy the same features that are already available in C but with language-specific assertions.
ghostwriter 6y ago
> (Formally verified is shifting the goal posts here: the bar is just "has a native library".) It is, but it is for a good reason - ATS formally verifies your safe functions, so you only need to implement your proof once and make a compiler agree with you, and then you can save on a community-driven code-review process. Rust, on the other hand, provides safety guarantees only for a subset of safe guarantees that ATS provides. Pointer manipulations have to reside in "unsafe" blocks, and that leads to CVEs - https://gts3.org/2019/cve-2018-1000657.html https://gts3.org/2019/cve-2018-1000657.html
- 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.

by dbaupp 6y ago

rumanator 6y ago

> 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. The dramatic nature of that difference is whether that library exists or not. Odds are, if exists then it's written in C. Thus this point is mute with regards to Rust because at best it's relegated to a nice-to-have, in the sense you can enjoy the same features that are already available in C but with language-specific assertions.

ghostwriter 6y ago

> (Formally verified is shifting the goal posts here: the bar is just "has a native library".) It is, but it is for a good reason - ATS formally verifies your safe functions, so you only need to implement your proof once and make a compiler agree with you, and then you can save on a community-driven code-review process. Rust, on the other hand, provides safety guarantees only for a subset of safe guarantees that ATS provides. Pointer manipulations have to reside in "unsafe" blocks, and that leads to CVEs - https://gts3.org/2019/cve-2018-1000657.html https://gts3.org/2019/cve-2018-1000657.html

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.