The cartoonist Dick Guindon famously wrote as follows. Writing is nature's way of letting you know how sloppy your thinking is. The number 1 prefixing that is my addition. Programmers and sometime-mathematicians also know that there are further stages of the same idea. Programming is nature's way of letting you know how sloppy your writing is. Mathematical proof is nature's way of letting you know how sloppy your programming is. Machine-checked proof is nature's way of letting you know how sl...
