"A (Not So Gentle) Introduction To Systems Programming In ATS" by Aditya Siram

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.

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.

> 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) if you are interested. You just don't bother yourself with this theory, and neither should you when programming FP. You don't bother number theory and arithmetic (complex topics) when doing simple addition in your code, right? > But I'm very used to the POSIX interface and honestly programming against much else tends to get me out of my comfort zone a little too much Then maybe your starting point should rather be this [1]. (Although this book is rather about system unix programming in OCaml than about language itself. For learning the language its manual should fit pretty well [2], finding a sweet spot between a narrated book and a standard. Other good and more in-depth introductions are [3] and [4]). There is also a unikernel called mirage os which includes TCP stack and other stuff and

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 Haskell will evolve enough to allow me to write such a program. Otherwise I might end up using ATS, though honestly the syntax is so ugly.