Earlier quoted context omitted.
> No, adding unsafe Rust does not undermine the safety argument But it does, see my answer in the thread below regarding ring buffers - https://news.ycombinator.com/item?id=24337184 > Is this not also true of ATS? That is, if ATS code calls a C function that returns a pointer, how do you know how long that pointer is valid for and whether you're expected to free it? the C implementation needs to be known, then the si…
> 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 block First, 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 optimizatio…
I've never stated that there's such a capability. I was saying that unlike Rust, ATS can be used to gradually rewrite every C call into a safe and formally-verified equivalent function that has exactly the same performance and memory charactersitics as the original C function.