3 ms·
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 forma
by auggierose 4y ago
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.
- josephg 4y agoMaybe. 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?
- auggierose 4y agoIdeally (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?