Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

blog.adacore.com

Post reply on HN
Print view View original

81–90 of 124 posts

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

#81

Post by touisteur »

Jtsummers wrote: post #59
eatonphil wrote: post #9

This is a fantastic post! It'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've looked at. While it's been on my list for a while, I'm more curious to try out Ada now.

It'll take you less than a week to get proficient enough in it to make something useful, or at least interesting. It's a very straightforward language, overall. https://learn.adacore.com/ - Pretty much the best free source until you're actually ready to commit to the language. The "Introduction to Ada" course took me maybe a week of 1-2 hours a day reading and practicing to go through. There's also a SPARK course tha…

Also, don't hesitate to use Rosetta Code to find useful little snippets. Not all perfect but a good jump-start.

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

#83

Post by touisteur »

JadeNB wrote: post #29
FrozenVoid wrote: post #11

Combsort 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.

Yes (co-author here) that was exactly the point. Thanks for putting it clearly.

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

#84

Post by touisteur »

fweimer wrote: post #79

Isn'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.

It was touched upon in the post: 'Tip: Don’t prove what you don’t need to prove' (and surrounding text). With a link on another proof for another sorting algorithm.

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

#85

Post by Jtsummers »

touisteur wrote: post #81
Jtsummers wrote: post #59

Earlier quoted context omitted.

It'll take you less than a week to get proficient enough in it to make something useful, or at least interesting. It's a very straightforward language, overall. https://learn.adacore.com/ - Pretty much the best free source until you're actually ready to commit to the language. The "Introduction to Ada" course took me maybe a week of 1-2 hours a day reading and practicing to go through. There's also a SPARK course tha…

Also, don't hesitate to use Rosetta Code to find useful little snippets. Not all perfect but a good jump-start.

Yep, I wrote a bunch of those RC examples too. It was a useful exercise when I decided to learn Ada (and with other languages, too).

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

#86

Post by yannickmoy »

twawaaay wrote: post #45
eranation wrote: post #44

Earlier quoted context omitted.

That is pretty awesome if you came up with this exact algorithm a decade ago, ( it was published in 2021, but apparently was in the wild in 2015[1] and I assume discovered earlier, but no one thought it was interesting enough to publish). Why didn’t you use bubble sort / insertion sort? (The algorithm in the paper looks like bubble sort at first look but is basically a clever insertion sort) what was the benefit of u…

I am not sure how awesome it is. It looks like something you can stumble on your own by accident on a whiteboard on an interview and use successfully even if you don't know why it works exactly. Honestly, I always thought it is a common knowledge and it is just too simple and for this reason gets omitted from books. People in CS/IT tend to not spend a lot of time on algorithms with bad complexity and so I am used to…

For a related eye-opening result, with both practical application and interesting research backing it, see this talk on "Quicksorts of the 21st century" at Newton Institute on Verified Software last year: https://www.newton.ac.uk/seminar/30504/

TLDR; practical complexity computation needs to take into account things like memory access latency on different architectures.

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

#88

Post by yannickmoy »

touisteur wrote: post #84
fweimer wrote: post #79

Isn'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.

It was touched upon in the post: 'Tip: Don’t prove what you don’t need to prove' (and surrounding text). With a link on another proof for another sorting algorithm.

and there are actually multiple ways to prove that the result is a permutation of the entry, either by computing a model multiset (a.k.a. bag) of the value on entry and exit and showing they are equal, or by exhibiting the permutation to apply to the entry value to get the exit value (typically by building this permutation as the algorithm swaps value, in ghost code), etc.

but none of this makes a good read for people not already familiar with program proof tools.

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

#89

Post by yannickmoy »

im3w1l wrote: post #64
ufo wrote: post #19

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. Does anyone here also use SPARK for this sort of thing? Are there other formal methods tools you'd use if you had to prove something like this?

Yeah, I see this as a very interesting reply to the TLA+ post. Might spend my evening diving into Ada and Spark. Edit: Some things I noticed. The package gnat-12 does not have gnatprove. Ada mode for emacs requires a compilation step that failes with gnat community edition. With alire there is no system gnat so it cannot compile it (quite possible I'm missing something). In the end I gave up on using emacs. Gnatstudi…

you can ask Alire to install the latest GNAT it built, or to use another version installed on your machine, see https://alire.ada.dev/transition_from_gnat_community.html

It also explains how to install GNATprove: ``alr with gnatprove``

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

#90

Post by MrYellowP »

blueflow wrote: post #4
roenxi wrote: post #3

If it looks "obviously wrong" 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). EDIT ^W^W^W Nope, I'm wrong. I did a worked example on paper. I think the devious thing here is the algorithm looks simple at a lazy glan…

This somewhat looks like bubble-sort minus the early exit.

It is BubbleSort. At least that's how I've learned it in the 80s.
Post reply on HN