I can’t believe that I can prove that it can sort

He starts from the wrong axiom that its hard to prove and creates a lot of nonsense over that.<p>Its requires just two induction proofs: - One that for I=1, after N comparisons the largest number is at position 1 (Proven with induction) its the base case - The other, that for any I=n+1 if we assume that the first n slots are ordered we can treat n+1 as a new array of length N-n and solve using the base case proof.<p>Talking about computer science and not doing the bare minimum of computer science is peak software engineering :)

Here is how it looks. <a href="https:&#x2F;&#x2F;xosh.org&#x2F;VisualizingSorts&#x2F;sorting.html#IYZwngdgxgBAZgV2gFwJYHsIwgUwO4DK6ATsgBTDHEA0MAJscHgJQwDeAUDFJiMtjAC8MSsQB0AGxwQA5sgAWAbi5wSMMlP6pBABkUxUAHgj7UAajOtOMeGo05+AK137Hx1xatcbqOOtEA2qgAujCGIlQBjsFeNjYgeMAADhRUtKi0jszKcSKJqPwMTKk0MADM6dRZOTYAvt71MPW1QA" rel="nofollow">https:&#x2F;&#x2F;xosh.org&#x2F;VisualizingSorts&#x2F;sorting.html#IYZwngdgxgBAZ...</a><p>If you compare it with both Insertion and Bubble sort. You can see it looks more like insertion sort than bubble sort.

I 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.<p>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, algorithmic complexity isn&#x27;t everything.

If it looks &quot;obviously wrong&quot; the quick proof that it works ... the j loop will move the largest unsorted element in the array into a sorted position. Since the i loop executes the j loop n times, the array must be sorted (since the n largest elements will be in the correct order).<p><i>EDIT</i><p>^W^W^W<p>Nope, I&#x27;m wrong. I did a worked example on paper. I think the devious thing here is the algorithm looks simple at a lazy glance.<p>To sort: 4-3-6-9-1, next round pivot for the <i>i</i> loop in [].<p><pre><code> [4]-3-6-9-1 9-[3]-4-6-1 3-9-[4]-6-1 3-4-9-[6]-1 3-4-6-9-[1] 1-2-3-6-9 &amp; sorted </code></pre> I can see that it sorts everything to the left of a pivot, then because it does that n times it comes to a sorted list. A reasonable proof will be more complicated than I thought.

The comments so far have tended to focus on the proof itself, but for me the coolest part of the blog post were the formal methods.<p>Does anyone here also use SPARK for this sort of thing? Are there other formal methods tools you&#x27;d use if you had to prove something like this?

I&#x27;ve been watching those mesmerizing YouTube videos visualizing sorting algorithms lately. The header of this article uses a screen cap from one of them.<p>Them: So what shows do you watch?<p>Me: ... It&#x27;s complicated.<p>There are a lot of different sorting algorithms. Like, <i>a lot</i>, a lot.<p>As I watch them, I try to figure out what they were optimizing for. Some only scan in one direction. Some only use the swap operation. Some seem to do the minimum number of writes. Some are incremental performance improvements over others.<p>When I see an algorithm like this, I don&#x27;t assume the person who wrote it was an idiot. I assume they were optimizing for something that&#x27;s not obvious to me. Its only modifying operation is swap, so maybe that operation is faster than an arbitrary insert for whatever system or data structure they&#x27;re using. There are no temporary variables besides loop counters, so maybe they&#x27;re on a memory-constrained environment. There&#x27;s barely any code here, so maybe this is for a microcontroller with precious little ROM. Or maybe they&#x27;re applying this as a binary patch and they have a strict ceiling to the number of ops they can fit in.<p>Or maybe it&#x27;s just the first sorting algorithm they could think of in an environment that doesn&#x27;t ship with one and the performance is adequate for their needs. In that case, it&#x27;s optimized for developer time and productivity. And honestly, it&#x27;s a far more elegant algorithm than my &quot;naive&quot; version would be.<p>These are all valid reasons to use a &quot;naive&quot; sorting algorithm.

This is a fantastic post! It&#x27;s great to have a concrete example of proving a not-trivial algorithm. And somehow this Ada code feels more approachable to me than HOL4 and other functional proof assistants I&#x27;ve looked at.<p>While it&#x27;s been on my list for a while, I&#x27;m more curious to try out Ada now.

The paper discussed on HN:<p><a href="https:&#x2F;&#x2F;news.ycombinator.com&#x2F;item?id=28758106" rel="nofollow">https:&#x2F;&#x2F;news.ycombinator.com&#x2F;item?id=28758106</a> (318 comments)

Why is this algorithm at all surprising?<p>(I&#x27;m really not trying to brag - I assume I must be missing something, that I&#x27;m naïve to think it obviously works, and it actually works for a different reason.)<p>In plain English - &#x27;for every element, compare to every element, and swap position if necessary&#x27; - .. of course that works? It&#x27;s as brute force as you can get?

Is this not a standard sorting algorithm? If I&#x27;m not mistaken this is my coworkers go to sort when writing custom sorts.

I taught myself this exact algorithm at 8 or 10 by sorting playing cards (we established an order for the kind, diamond &lt; leaf &lt; spades &lt; heart) in a very very very long plane trip where I had neglected to bring comic books or something.

After each outer loop iteration, A[:i] (the array up to i) is in ascending order with the max of A at A[i].<p>This is true the first iteration since max(A) is eventually swapped to A[1]. This is true in subsequent iterations since during the ith iteration, it inserts the next element, initially at A[i], into A[:i-1] and shift everything up with swaps with A[i] so A[:i] is sorted, with the max of A moved to A[i]. After that no more swaps happen in the ith iteration since A[i] contains the max of A.

Isn&#x27;t the proof incomplete because it does not ensure that the result is a permutation of the original array contents? Just overwriting the entire array with its first element should still satisfy the post-condition as specified, but is obviously not a valid sorting implementation.

Article says it is better to actually read the paper instead of trying to figure it out.<p>I disagree on that. It is a good exercise to try to prove it by yourself and it was actually quite fun<p>Main mistakes author makes though<p>- trying to prove it works without first understanding why &#x2F; how it works. Always simulate test-runs on paper &#x2F; in your head before<p>- trying to prove on machine first. Always make sure you can do the proof on paper first. Then and only then should you battle with your verifier &#x2F; solver to get it to understand your proof

Interesting. It is a bit counter intuitive at first but not too hard to see how it works.<p>After the first main loop, the first item will be the biggest item in the list.<p>The inner loop, as it always starts from 1 again will gradually replace the bigger items with smaller items, and so on.

Every time somebody proves that a sorting algorithm sorts, they forget to prove that the algorithm doesn&#x27;t just drop values or fill the entire array with 0s (with fixed-length arrays, as here).<p>On paper: &quot;it&#x27;s just swaps&quot; Formally: &quot;how do I even specify this?&quot;<p>(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&#x27;s transitive, and show it&#x27;s preserved by swap.)

Small sort implementation in ES6:<p><pre><code> const args = process.argv.slice(2).map(Number); for (let i = 0; i &lt; args.length; i++) for (let j = 0; j &lt; args.length; j++) if (args[i] &lt; args[j]) [args[i], args[j]] = [args[j], args[i]]; console.log(args.join(&#x27; &#x27;)); </code></pre> Didn&#x27;t expect it to be actually that simple, but now that I wrote it, it makes complete sense.<p>To PROVE it, is another thing. Good work.

TFA seems to be a somewhat wasteful version of an algo which in my mind I call &#x27;sinkersort&#x27; or &#x27;minsort&#x27;:<p><pre><code> for (i=0; i&lt;n; ++i) for (j=i+1; j&lt;n; ++j) if (a[j] &lt; a[i]) swap(a[j], a[i]); </code></pre> Here the inner loop basically finds a min value of the remaining subset. This progressively fills the array in the sorted order.<p>The number of comparisons is bound by n^2&#x2F;2 vs n^2 of TFA.

a &quot;new sorting algorithm&quot;? Pretty sure it existed 50 years ago.

Vaguely remember seeing this in the first few chapters somewhere of Spirit of C by Mullish and Cooper.

Wow, I wish we had these built-in provers in VHDL (which is basically Ada in sheep&#x27;s clothing).

&gt; published at the end of 2021<p>I&#x27;m so confused. That &quot;new&quot; algorithm is just BubbleSort?

Combsort is far more elegant and faster algorithm. I&#x27;ve wrote a type-generic combsort a while ago here: <a href="https:&#x2F;&#x2F;github.com&#x2F;FrozenVoid&#x2F;combsort.h" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;FrozenVoid&#x2F;combsort.h</a><p>(Combsort as well as mentioned algorithm also consists of two loops and a swap)

Isn&#x27;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?

So, <i>Lionel</i> knew how to implement a 3D Renderer, but had no clue about O(n) complexity neither other sorting algorithms? I am buffled