"A (Not So Gentle) Introduction To Systems Programming In ATS" by Aditya Siram
Why Hacker News recommends it
Cited in Rust and systems-language threads as the best introduction to ATS, a language claimed to go beyond Rust's safety guarantees.
What it is
Aditya Siram introduces ATS, a statically typed ML-like language that compiles to C and offers type-safe pointer arithmetic and a full proof language. The Strange Loop talk shows off C interop, concurrency and verification features with non-trivial examples.
Recommended by 4 HN commenters across 4 different months, 2017 to 2022.
What Hacker News said
Recommends wahern · 2017-10 · on “Building on Rock, Not Sand”
> Without these, you simply can’t have a fast, > memory-safe language: either you surrender > speed, by boxing everything, or you surrender safety. Not only can you have speed and safety without Rust's rigid enforcement of exclusive ownership, you can do even better--even faster and with even stronger security guarantees: [this video] [LINK]
Recommends wahern · 2017-10 · on “Building on Rock, Not Sand”
How many buffer overflows were involved in the Equifax leak? The ultimate solution to the problem is formal verification. Rust solves this for buffer overflows, but nothing else. It's a one trick pony. Someone posted this interesting nugget on HN the other day: [this video] Aside from some of the awkward ergonomics, its mechanism for formal specification looks brilliant. And you get to keep C's bag-of-bytes object manipulation and pointer arithmetic (when you want it) without having to resort to unsafe{}. For projects where it's worth the effort to carefully declare precise typing semantics (because safety, performance, whatever), I want a wholistic solution. Otherwise my time and money is better
Recommends snaky · 2018-09 · on “How did software get so reliable without proof? (1996) [pdf]”
If you are interesting in a programming language suitable for system level programming, and using proving techniques, maybe ATS would be of interest. [this video] [LINK]
Recommends Athas · 2020-08 · on “Supporting Linux kernel development in Rust”
Yes, ATS can guarantee all those things and more. In particular, ATS allows you to write "unsafe" code, which you then prove safe with a mechanically verified proof. This is in contrast to unsafe Rust, which depends on programmer discipline, and has no (intra-language) mechanism for verification beyond the basic type system. You could say that Rust is all-or-nothing, while ATS allows gradual verification, as well as proving safe much more complex code than you can in Rust. I'm not going to claim that ATS is overall better than Rust - it's not - but it's a far more powerful language than Rust for safe systems programming. It's just that most people are not willing or able to pay the very high
Recommends rtfeldman · 2021-08 · on “The ATS Programming Language”
Some entertaining talks introducing the language, by /u/deech: "A Tase Of ATS" at Compose Conf 2019: [LINK] "A (Not So Gentle) Introduction To Systems Programming In ATS" at Strange Loop 2017: [this video]
Cites masklinn · 2017-10 · on “Fun facts about Rust's growing popularity”
> So if you just want a native language with a good type system and a growing ecosystem, where do you go? Still Rust or something else? [this video]
Cites ernst_klim · 2019-08 · on “Rust 1.37.0”
> I guess I still find FP very abstract as a concept. I'm starting to like the notion of immutability as a design goal. I'm rather asking about OCaml or SML than about something abstract matters like denotational semantics, system-F or pure lambda calculus. There are pretty much the same abstract concepts behind imperative programming languages as well: operational semantics, Turing machines, which, I argue, are even more complex. And if you write OOP, you have to deal with open recursion, covariant/invariant/contravariant subtyping relations, late bindings, polymorphic self type etc etc. There is a book called ``Theory of objects'' by Luca Cardelli (who is guilty for both SML and C++, BTW)
Cites reirob · 2019-10 · on “Google Is Uncovering Hundreds of Race Conditions Within the Linux Kernel”
ATS language. It compiles to C and I believe I have seen even that experimentally some kernel module was developped in it. Here some resources: The Wikipedia page: [LINK] "A (Not So Gentle) Introduction To Systems Programming In ATS" by Aditya Siram at the StrangeLoop 2017: [this video] Introduction to ATS, a series of screen casts: [LINK] I do not program in ATS because I am not doing anything that needs to be as efficient, so that I have the luxury to enjoy programming and learning Haskell, in the hope that by the time when I would need to write some super secure and performant program that has to run without interruption, and is used by more users than myself, well, I hope that by that time Ha