Strange Loop Conference
4 HN recommenders · recommended in 9 months, 2017–2022
36:58 · 26K views · Sep 30, 2017
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.
Cited in Rust and systems-language threads as the best introduction to ATS, a language claimed to go beyond Rust's safety guarantees.
11 comments from Hacker News
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 price in ergonomics. I recommend watching this presentation for a good idea of what ATS programming is like: this video In short, it's about as user-friendly as an overheating nuclear reactor.
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 spent throwing Javascript or Python at the problem, which solve the buffer overflow problem just as well.
> 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]
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
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]