(Derailing this troll-initiated thread a bit with a serious answer) > what’s the formula for quicksort That is expressible! It’s what one would write in a pro

(Derailing this troll-initiated thread a bit with a serious answer) > what’s the formula for quicksort That is expressible! It’s what one would write in a proof assistant or powerful type system such as Coq, Agda, Idris. The formula is the algorithm, the type is the theorem (quicksort has type any-list and maps it to sorted-list, or in code – literally – `quicksort : Ordering(A) -> List(A) -> SortedList(A)`).