For formal proofs the effort scales quadratically, does Rust code also become quadratically slower with some constant factor? I'd assume runtime-checks could provide statistical safety and each component may need statistics tweaking unless being small enough/verified/edge cases enumerable with reasonable certainty etc. Are you aware of any known statistics or work besides the 0,x bugs per 1000 lines of code taking into account classes of bugs? Or what is your take on this?
All of them, with the notable exception of tigerbeetle, a financial transactions database, have issue trackers which are littered with users reporting segfaults. I don’t really know if it’s more common than in popular Rust repositories, but this is my highly anecdotal, qualitative investigation.
What worries me is that when you dig into specific issues for root causes, there seem to be a lot of different root causes and not a lot of obvious fixes. And segfaults are just the tip of the iceberg, the most obvious memory errors. I don’t think people are reporting heap corruption in the same way, if ever.