> Borrow checking is basically a synonym for affine type system.
No? It's more akin to flow analysis with special generic types called lifetimes.
> The same outcome can be achieved via affine types, linear types, effects, dependent types, regions, proofs, among many other CS research in type systems.
Sure, and sounds, colors, and instruments are the same, but they are mixed to create an audio-video song. I'm not saying that what Rust did is something that came about ex nihilo, without precedence.
But having it all unified uniquely the way Rust did it is frankly revolutionary. Until now, people assumed if you want memory safety, you have to add a GC (tracing or RC). Or alternatively write extensive proofs about types like Ada/Spark.