[solomatov]

I think even D, Rust, and others aren't enough especially taking into account the damage such bugs cause. We should switch to dependently typed languages like Idirs and require complete proof of correctness for such important algorithm.

Dependently typed programming languages aren't yet ready to be used for general purpose programming, however, they are practical enough to verify correctness of isolated algorithms. We actually, have used them at JetBrains to verify correctness of collaborative editing algorithms. You won't believe how many "stupid" mistakes seemingly well tested code contains.