5 ms·

Your centering your criticism of ATS on popularity. Does an investment on PR trumps technical merit?

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.)
chinigo 6y ago
Popularity != PR. Choosing an obscure language with little community support imposes real-world development costs: it's harder to find or ramp up new developers, there are fewer eyes identifying bugs in the implementation, tooling support can be subpar, documentation and blog posts are harder to find, etc. (btw I know nothing about ATS so I'm not saying this is a good description of that language in particular.)
- ghostwriter 6y ago
  I agree with your points regarding tooling and dev support in general. ATS, in that regard, benefits from being a "frontend compiler" to GCC - all the tooling for GCC can be used equally well for ATS codebases. Developers need to know C well (not an issue with all the learning material available), and at least one language from ML family (OCaml, Standard ML, F#, Haskell to some extent) to quickly pick up the syntax and common recursive constructs. There are three great books [1] available online, and a collection of common system programming examples that demonstrate how data types and algorithms can leverage safe language features [2] [1] http://www.ats-lang.org/Documents.html http://www.ats-lang.org/Documents.html [2] http://ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/ http://ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/
outworlder 6y ago
> Does an investment on PR trumps technical merit? If PR == popularity, yes. Otherwise we would all be writing our stuff in Haskell, Lisp, Elm, F# and similar, and Algol-derived languages would be a footnote at this point.
Twirrim 6y ago
Yes, it really does if you're talking about success. Just like with Betamax vs VHS, and many, many other examples over the years. Technical merit is only one small part of a success story, and it's not the most important one.
stmw 6y ago
Popularity is not quite the same as PR. But yes, it's about the number of engineers and projects using it, and the growth of such adoption. If technical merits were the only criteria for making a difference, I think it's fair to say we would have a very different technology ecosystem today. :)

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

chinigo 6y ago

Popularity != PR. Choosing an obscure language with little community support imposes real-world development costs: it's harder to find or ramp up new developers, there are fewer eyes identifying bugs in the implementation, tooling support can be subpar, documentation and blog posts are harder to find, etc. (btw I know nothing about ATS so I'm not saying this is a good description of that language in particular.)

ghostwriter 6y ago
I agree with your points regarding tooling and dev support in general. ATS, in that regard, benefits from being a "frontend compiler" to GCC - all the tooling for GCC can be used equally well for ATS codebases. Developers need to know C well (not an issue with all the learning material available), and at least one language from ML family (OCaml, Standard ML, F#, Haskell to some extent) to quickly pick up the syntax and common recursive constructs. There are three great books [1] available online, and a collection of common system programming examples that demonstrate how data types and algorithms can leverage safe language features [2] [1] http://www.ats-lang.org/Documents.html http://www.ats-lang.org/Documents.html [2] http://ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/ http://ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/

outworlder 6y ago

> Does an investment on PR trumps technical merit? If PR == popularity, yes. Otherwise we would all be writing our stuff in Haskell, Lisp, Elm, F# and similar, and Algol-derived languages would be a footnote at this point.

Twirrim 6y ago

Yes, it really does if you're talking about success. Just like with Betamax vs VHS, and many, many other examples over the years. Technical merit is only one small part of a success story, and it's not the most important one.

stmw 6y ago

Popularity is not quite the same as PR. But yes, it's about the number of engineers and projects using it, and the growth of such adoption. If technical merits were the only criteria for making a difference, I think it's fair to say we would have a very different technology ecosystem today. :)