Formally verifying a whitespace cleanup editor function in Coq! https://c9x.me/articles/trust/