Maybe it is time to do some theorem proving for code like this.
Also shows the obvious waste in modern software development: A decade is plenty of time to formally verify a dozen such algorithms. We need to make it easier to do it in a production environment.
Maybe. I honestly don’t know enough about theorum proving.
One nice thing about fuzz testing is that it tests both the concepts and the specific implementation. Probably 70% of bugs my fuzzers have found over the years are edge cases my code is handling incorrectly. If I made a “pure” model of my sync engine, wouldn’t I also, still, need to prove my actual implementation matches that model?
Ideally (part of) your model would already be executable, so that there is no separate implementation. Why have a separate implementation in C, JS, Java, Go, Dart, Swift, Rust, ..., if you have already something much cleaner which you have proven to be correct?
