Overall not easy to read article. Quite confusing. It makes case rather rewriting in Rust* should instead rewrite in formal spec and generate the code, which is now easier due to LLMs, but why that code cannot be Rust? The memory model and structure may make Rust better AI target and helpful in cases human intervention is required.