Sorting algorithms are to computer science what “Hello World!” is to programming. A way for beginners to get their hands dirty. Which also means t

I can’t believe that I can prove that it can sort | The AdaCore Blog

submited by

Style Pass

2022-07-01 19:30:13

Sorting algorithms are to computer science what “Hello World!” is to programming. A way for beginners to get their hands dirty. Which also means that most programmers don’t write “Hello World!” programs past their studies, and computer scientists don’t look at sorting algorithms past their PhD.

Which made it surprising that a new “interesting” sorting algorithm was published at the end of 2021, whose appeal drew attention from both computer scientists and programmers. Here is the algorithm in full details:

As an expert user of Ada, and an anecdotal user of SPARK, one of us (Lionel) took it as a challenge to try some functional proof with SPARK. Despite a hopeful start, this ended up badly. As a SPARK expert thus contacted to help with the challenge, one of us (Yannick) took it as a way to show how functional proof should be approached in SPARK. Including some false starts, this ended up well (and under an hour). This is the story of this challenge, and the tips we think are important to share with those who aim at functional proof with SPARK.

I read the paper intro, and couldn’t realize what was wrong with it instinctively, but quickly seeing all the replies to the tweet brought back memories of learning programming, writing cool (at the time) programs for years, and then later on getting some formal computer science education.