Tons of languages have soundness bugs. While that one is ten years old, there have been zero reports of it ever being found in the wild, and it will finally be fixed relatively soon.
Yes. For various other reasons, the trait system needed to be rewritten, and it would also end up fixing this. Since it’s essentially a theoretical issue, spending time on this wouldn’t make sense. In the meantime, that rewrite is nearing completion. The most recent version of rust uses it for coherence checking. The next few months are likely to remove several other stoppers from moving forward. It’s almost time for a crater run, and then fixing whatever issues that shows up.
The Rust one seems a specific bug in the implementation, while the Agda one seems more like a fundamental flaw caused by allowing aliased mutation though.