See e.g. https://bluishcoder.co.nz/2010/06/02/safer-c-code-using-ats....
That said, thanks for your work on Rust! Count me a big fan of the language.
Also, I think saying that the ATS has no unsafe{} sections is misleading: it isn't explicitly marked in the source, but the compiler still cannot check the "ownership" annotations in the imports are correct, or that, say, the preconditions of the functions (which may lead to undefined behaviour when violated) are satisfied. In other words, all of that code is implicitly surrounded in an `unsafe` block.
A Rust API designed for people to use will also not have unsafe code, e.g. https://blog.rust-lang.org/2015/04/24/Rust-Once-Run-Everywhe...
(The linearity is essentially handled by destructors: the common case is the clean-up is just that, clean-up, and so destructors work well. It is definitely more annoying to 100%-type-check APIs that have more interesting clean-up/closing procedures but these are rarer.)
You end up with a definition that checks at compile time that:
* We don't exceed the memory bounds of the source buffer
* We don't exceed the memory bounds of the destination buffer
* The destination buffer is at least the minimium size required by the function documentation
* We can't treat the destination buffer as a string if the function fails
* We can't treat the destination buffer as an array of bytes if the function succeeds
* Off by one errors due to null terminator handling are removed
* Checking to see if the function call failed is enforced
And there's no overhead at runtime.