[qsort]

Sure, but I agree with parent's comment that it's a... weird turn?

When one introduces transition systems, I usually expect "yeah, now he's going to define a labeled transition system, then introduce modal logic, maybe temporal logic, definitely bisimulations, maybe Van Benthem".

Obviously one can do proofs of elementary algorithms with that formalism, it's just a bit unusual, that's all.

[rain1]

your literally named qsort why are you complaining

[NDizzle]

When it rains, it pours?!