3 ms·
Every time somebody proves that a sorting algorithm sorts, they forget to prove that the algorithm doesn't just drop values or fill the entire array with 0s (wi
by fdupress 4y ago
Every time somebody proves that a sorting algorithm sorts, they forget to prove that the algorithm doesn't just drop values or fill the entire array with 0s (with fixed-length arrays, as here).
On paper: "it's just swaps"
Formally: "how do I even specify this?"
(For every value e of the element type original array and the final array have the same number of occurrences of e. Show that that's transitive, and show it's preserved by swap.)
- touisteur 4y agoHi, co-author here. We actually touched upon this subject in the article: 'Tip: Don’t prove what you don’t need to prove' and surrounding text. Also previous comment by Yannick: https://news.ycombinator.com/item?id=31980126 https://news.ycombinator.com/item?id=31980126
- fdupress 4y agoLooked for it and missed it. And thanks for writing this up, by the way. Having people less familiar with formal methods try and write up their experiences is, I think, much more effective at letting people in than having experts try and write tutorials.