3 ms·

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

• steveklabnik 2y ago
  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 2y ago
    > 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."
    • steveklabnik 2y ago
      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.
• SkiFire13 2y ago
  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.