See also: I can’t believe that I can prove that it can sort - https://news.ycombinator.com/item?id=31975507 https://news.ycombinator.com/item?id=31975507 - Jul

See also: I can’t believe that I can prove that it can sort - https://news.ycombinator.com/item?id=31975507 https://news.ycombinator.com/item?id=31975507 - Jul 2022 (115 comments) Here's some other sorting algorithms proven with SPARK, with much more straightforward proofs: https://github.com/AdaCore/spark2014/blob/master/testsuite/gnatprove/tests/281__sorts/main.adb https://github.com/AdaCore/spark2014/blob/master/testsuite/g...