I have connections with the academic GC community. I gave an invited talk at ISMM 2012. I guarantee that they will not agree "Rust is a garbage-collected language".
FWIW Wikipedia describes "garbage collection" as "a form of automatic memory management" and goes on to say "Other similar techniques include stack allocation, region inference, memory ownership ..." so whoever wrote that doesn't agree that all forms of automatic reclamation are garbage collection.
I prefer to avoid arguing about the meaning of words but it's not good to sow confusion.
> Are the several multi-100-kloc ats compilers out there not real-world enough?
Yes, projects written by the creators of the language are not enough.
> If not then, on the topic of proof languages, ada/spark and isabelle/hol had proven themselves long before rust.
FWIW Wikipedia describes "garbage collection" as "a form of automatic memory management" and goes on to say "Other similar techniques include stack allocation, region inference, memory ownership ..." so whoever wrote that doesn't agree that all forms of automatic reclamation are garbage collection.
I prefer to avoid arguing about the meaning of words but it's not good to sow confusion.
> Are the several multi-100-kloc ats compilers out there not real-world enough?
Yes, projects written by the creators of the language are not enough.
> If not then, on the topic of proof languages, ada/spark and isabelle/hol had proven themselves long before rust.
Before Rust, Ada/SPARK didn't support dynamic deallocation. See https://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memo..., which cites Rust.
SeL4 required 200K lines of Isabelle/HOL proofs to verify 7.5K lines of C; that approach simply doesn't scale.