Quicksort without pseudo code and building code against functional specifications

Mostly for my own amusement, I wanted to see if it was possible to specify basic sorting algorithms in ordinary algebra without ”formal methods” or either pseudo or genuine code. Functional programming people try to do this using functional programming languages and it’s all been done in Lisp, but the goal here was to just use recursive functions and sequences and to see whether it made things clearer or not. I think it makes things clearer but you can judge for yourself. The paper starts with basic methods and selection sort, then quicksort, insertion sort, and merge sort before looking at radix sort. There is a discussion and a pedantic appendix with all the definitions and
obvious lemmas . There’s code too.