5 ms·

Popularity and momentum translate into (and are proxies for) important things like: library availability, long-term maintenance and support, more edge cases are

by dbaupp 6y ago

Popularity and momentum translate into (and are proxies for) important things like: library availability, long-term maintenance and support, more edge cases are explored (so less “research”, breaking new ground and bugs when going off the beaten track), tooling and even availability of teaching material like documentation and tutorials.

ghostwriter 6y ago
In case of ATS, any C library can be treated as a "unsafe-marked" ATS library, so there's no problem with library support, the problem is with their formal verification. And Rust libraries regularly suffer from the same lack of formally-verified and proven-to-be-safe APIs.
- 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.
- dbaupp 6y ago
  Ah, furthermore, looking at a comment below, it seems ATS's support for C libraries is almost identical to Rust's: specify a list of functions and their signatures on the ATS/Rust side. From your adoring descriptions, I had been assuming it simplified the process properly, by allowing importing a C header directly (like Swift can). (The main difference seems to be ATS allows inline C, since it looks to be tied to C as a compilation target.)

by dbaupp 6y ago

ghostwriter 6y ago

In case of ATS, any C library can be treated as a "unsafe-marked" ATS library, so there's no problem with library support, the problem is with their formal verification. And Rust libraries regularly suffer from the same lack of formally-verified and proven-to-be-safe APIs.

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.
dbaupp 6y ago
Ah, furthermore, looking at a comment below, it seems ATS's support for C libraries is almost identical to Rust's: specify a list of functions and their signatures on the ATS/Rust side. From your adoring descriptions, I had been assuming it simplified the process properly, by allowing importing a C header directly (like Swift can). (The main difference seems to be ATS allows inline C, since it looks to be tied to C as a compilation target.)