> Safety isn’t the presence of safe constructs, but the absence of unsafe ones. Exactly. Here is a data point: https://spinroot.com/spin/Doc/rax.pdf https://s

> Safety isn’t the presence of safe constructs, but the absence of unsafe ones. Exactly. Here is a data point: https://spinroot.com/spin/Doc/rax.pdf https://spinroot.com/spin/Doc/rax.pdf Tl;DR: This was software that ran on a spacecraft. Specifically designed to be safe, formally analyzed, and tested out the wazoo, but nonetheless failed in flight because someone did an end-run around the safe constructs to get something to work, which ended up producing a race condition.