I previously blogged about the ICan’tBelieveItCanSort algorithm, which is a weird insertion sort-like algorithm that defies all common sense and somehow sorts arrays. Well, if you read that post and watch the visualization a few times, it should make more intuitive sense why it works.
Kublai: Hey, I don’t believe you! Your visualization looks pretty cool, but how can you be sure this wacky algorithm works for all inputs?
Glad you asked! To dispel all doubt, here’s a formal proof.
Kublai: Oh no, not a scary scary formal proof! I don’t wanna trudge through tons of lines of tedious reasoning like in the original arXiv paper for ICan’tBelieveItCanSort!
Don’t worry, my proof uses the Dafny verification language, which helpfully automates some tedious proof steps with features like automatic induction. It’s only a few additional lines! (Sorry for the weird syntax highlighting, since my static site generator doesn’t recognize Dafny as a language.)
method ICan'tBelieveItCanSort(A: array<int>)
modifies A
// Output must be same element as original array
// Otherwise we could cheat and just return 1, 2, ... A.Length
ensures multiset(A[..]) == multiset(old(A[..]))
// Output should be nondecreasing
ensures forall i :: 0 < i < A.Length ==> A[i - 1] <= A[i]
{
ghost var orig := multiset(A[..]);
for i := 0 to A.Length
invariant multiset(A[..]) == orig
// Current prefix should be nondecreasing
invariant forall i' :: 0 < i' < i ==> A[i' - 1] <= A[i']
{
for j := 0 to A.Length
invariant multiset(A[..]) == orig
// A[i] always stores largest element so far
invariant forall j' :: 0 <= j' < j ==> A[j'] <= A[i]
// Don't screw up the current prefix
invariant forall i' :: 0 < i' < i ==> A[i' - 1] <= A[i']
// Afterwards, the prefix will be correct, plus an additional A[i]
// So we can extend the current sorted prefix
{
if A[i] < A[j] {
A[i], A[j] := A[j], A[i];
}
}
}
}
Kublai: Whoa, that’s it? No tedious casework? Just some loop invariants? Dafny must be really magically smart or something!
Internally, Dafny uses the Boogie intermediate language and the Z3 SMT solver, so it’s not quite magic and sometimes you have to manually add extra proof steps to help it out. But when it works, Dafny definitely feels really futuristic and magical! Futuristic, as in I feel like the future of programming languages for software engineering will be having more and more compile-time checks to catch bugs, like Rust on steroids.
Kublai: Thosemultisetinvariants make perfect sense, but how’d you conjure up thoseforalllines?
If you stare long enough at the visualization in my previous post, you might notice some patterns, such as how the prefix A[0..i] seems to be sorted after iteration i. I just codified these observations and Dafny was able to prove it formally from there!
Anyways, let’s actually run our proved function!
Kublai: But why would you ever need to run a function if you already know it’s 100% correct, haha?
method Main() {
var A := new int[] [6, 1, 4, 5, 8, 9, 3];
// Or try a larger A
// var A := new int[1000](i => i * i % 1000);
ICan'tBelieveItCanSort(A);
for i := 0 to A.Length {
print A[i], "\n";
}
}
Now save all this code in a file and run it with dafny run. (I wasted a lot of time wondering why my code wasn’t running since I accidentally used main at first instead of Main, oops.) One cool thing about Dafny is that it can be translated to many languages such as Python and Rust using the -t flag.
Dafny seems more focused for software development rather than math proofs, but I haven’t proved any particularly complicated programs with it yet so I’m not sure how practically useful it is. Also, you need a special editor (i.e. VSCode with an extension) to ergonomically use Dafny’s gutter highlights and error squiggles (and feels a bit like Pluto.jl). At least I don’t have to write 10 times more lines of proofs than actual code!