retooted nmeum
For those interested in fooling around with niche compiler technology and programming languages: Here's a fun sketch of a correctness proof for Hare's sort::inplace stdlib function through symbolic execution of the QBE intermediate representation emitted by the Hare compiler.