> 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 invarian

> 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 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.