>
ring buffers in Rust use "unsafe" and at some point there was a logical CVE in vec_deque that broke one invariant of the unsafe blockFirst, you're talking about two different things here. Originally you were talking about incrementally adding Rust bindings to C code and how that obligated you to write "unsafe". Now you are talking about pure-Rust implementations of data structures that use "unsafe" for optimization purposes. The second one is much more dangerous.
Second, it does not undermine the safety argument - quite the opposite, as demonstrated by the fact that code that used VecDeque remained unchanged after the bug fix. Everything that the Rust compiler proved about code that used VecDeque, on the assumption that VecDeque was sound, remained just as proven after the bug was fixed and VecDeque was changed to be actually sound. There was no ex-falso-quodlibet problem. There was a clear delineation in the safety argument: on one side, a human was obligated to check that VecDeque was implemented soundly, and on the other side, the Rust compiler checked that every user of VecDeque did so soundly. The first part was done incorrectly and then fixed; the second part remained done correctly.
> the proof itself can indicate whether a pointer is stored/taken care of inside the C function or it should be taken care of outside the function (the latter is indicated by a prefixed "!" to the pointer type).
Then this is an axiom as input to the proof, not a proof itself. That is, ATS is no more capable than Rust of magically determining what the unstated invariants of C code are; it can only prove that certain things logically follow from certain assumptions. This is precisely what Rust does, too, except it is clearer than ATS because any use of such unchecked assumptions are clearly marked with the "unsafe" keyword.
In the linked ATS code, I see no indication, as a human reviewer, about which parts I should carefully audit (e.g., the annotation of the "extern fun") and which parts ATS has checked for me (e.g., the implementation of "string_to_base64"). In Rust, you can very quickly search a codebase for "unsafe" and see what needs auditing. (And in fact this technique empirically works well for finding unsoundness in production Rust code, and I can point to multiple examples of it. I wonder what people do when reviewing production ATS code.)
Again, I'm not saying ATS isn't cool. I'm not saying it wouldn't be great to have ATS support in the Linux kernel. Please work on this. There are, in fact, lots of things that ATS can do that Rust cannot do, and they are helpful to have. But I think the specific things you are claiming are things that Rust can do just fine or that ATS in fact cannot do.