Wow, I wish we had these built-in provers in VHDL (which is basically Ada in sheep's clothing).
They are there. You just have to pay a lot to the right companies.
I can’t believe that I can prove that it can sort
21–30 of 124 posts
Re: I can’t believe that I can prove that it can sort
#22Isn't the sorting algorithm in question the famous BubbleSort? I understand the value of formally proving it works, but why is the name mentioned nowhere?
Re: I can’t believe that I can prove that it can sort
#23Isn't the sorting algorithm in question the famous BubbleSort? I understand the value of formally proving it works, but why is the name mentioned nowhere?
[deleted]
Re: I can’t believe that I can prove that it can sort
#24Isn't the sorting algorithm in question the famous BubbleSort? I understand the value of formally proving it works, but why is the name mentioned nowhere?
Nope - here's the original paper on the algorithm in question: https://arxiv.org/pdf/2110.01111.pdf
Re: I can’t believe that I can prove that it can sort
#25Isn't the sorting algorithm in question the famous BubbleSort? I understand the value of formally proving it works, but why is the name mentioned nowhere?
No, it's not. Previously discussed on HN here: https://news.ycombinator.com/item?id=28758106 (https://arxiv.org/abs/2110.01111)
Re: I can’t believe that I can prove that it can sort
#26Isn't the sorting algorithm in question the famous BubbleSort? I understand the value of formally proving it works, but why is the name mentioned nowhere?
It feels similar at first blush but it's not really. In bubble sort you compare/swap adjacent elements, and exit if you make a pass through the collection without making any changes. Whereas this will compare/swap the element at every index to every other index, and just exits when it's done performing all those comparisons.
Re: I can’t believe that I can prove that it can sort
#27I actually used this algorithm a decade ago to implement a log-based, transactional database system for an embedded system with very low amount of memory and requirement that all memory be statically allocated. To the frustration of the rest of the development team who first called me an idiot (I was new) then they could not make quicksort run as fast on inputs that were capped at something like 500 items. Apparently…
I fee like anyone who was surprised that algorithmic complexity isn't everything, probably didn't totally understand it. The assumptions (like ignoring constants) are straight out of calculus limits. That (+10000) on the end doesn't mean anything if you're sorting an infinite list, but it means a lot if you're sorting 15 (or in your case 500) entries.
Re: I can’t believe that I can prove that it can sort
#28Here is how it looks. https://xosh.org/VisualizingSorts/sorting.html#IYZwngdgxgBAZ... If you compare it with both Insertion and Bubble sort. You can see it looks more like insertion sort than bubble sort.
And here's a version I wrote that visualizes it on your terminal https://github.com/radiantly/simplest-sort
Re: I can’t believe that I can prove that it can sort
#29Combsort is far more elegant and faster algorithm. I've wrote a type-generic combsort a while ago here: https://github.com/FrozenVoid/combsort.h (Combsort as well as mentioned algorithm also consists of two loops and a swap)
I don't think that the goal here is to show a fast and elegant sort, but rather to show that a sorting algorithm that seems like it can't possibly work actually does. That is, probably no-one will learn from this article how to sort better, but hopefully people will learn from this article how to formally prove things (e.g., about sorting) better.
Re: I can’t believe that I can prove that it can sort
#30I actually used this algorithm a decade ago to implement a log-based, transactional database system for an embedded system with very low amount of memory and requirement that all memory be statically allocated. To the frustration of the rest of the development team who first called me an idiot (I was new) then they could not make quicksort run as fast on inputs that were capped at something like 500 items. Apparently…
You sure it was this algorithm and not Bubble Sort?
> algorithmic complexity isn’t everything
Yeah very true. Or at least hopefully everyone knows that complexity analysis only applies to large n, and small inputs can change everything. In console video games it was very common to avoid dynamic allocation and to use bubble sort on small arrays. Also extremely common to avoid a sort completely and just do a linear search on the (small) array while querying, that can end up being much faster than sorting and binary searching, especially when the total number of queries or the number of queries per frame is also low.