[trott]

Yep, and even without dynamic memory management, Ada is not type-safe: https://www.enyo.de/fw/notes/ada-type-safety.html

Rust also has soundness holes, by the way. This one is almost 10 years old: https://github.com/rust-lang/rust/issues/25860

[steveklabnik]

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.

[trott]

> it will finally be fixed relatively soon

2015: "The work needed to close this has not yet landed. It's in the queue though, once we finish up rust-lang/rfcs#1214."

[SkiFire13]

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.