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

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: https://www.youtube.com/watch?v=zt0OQb1DBko https://www.youtube.com/watch?v=zt0OQb1DBko In short, it's about as user-friendly as an overheating nuclear reactor.