> If things are complicated enough that we actually need Agda/CoQ/Idris to 
     feel safe — seems that things went really wrong at some point.

I disagree. Complex software/hardware is by its nature full of bugs. What Rust set out to do is complex and it's bound to have bugs, but doesn't mean it's reason to abandon it, no more than we should discard LHC or ITER because they had issues starting up.

Whether it's a wrong invariant on TimSort or a really obscure multi-threading case, or a weird glitch in time library, its still an error. Each one is exploitable.

ALL software could use some coverage/tests and theorem proving. I just wish Rust started with a proven safe subset.

      > Exactly! And I'm just saying that a problem which is "not very likely to 
     trigger, but is very hard to find if happens" is far,   
     far more dangerous than a problem which is "easy for a 
     novice to miss, but every experienced developer would notice".

Again, I disagree. The matter of security is one about making the assailant less likely to breach your software. If you take two comparable pieces of code, the one with more holes will take less effort to break.

If your language offers fewer avenues of exploit, makes these exploits more expensive. A rare bug is worth more than a run of the mill bug. Which prohibits the number of assailants which could purchase it, which reduces number of potential attackers.