I don’t know much about about formal methods, so a while back I read Hillel Wayne’s post Let’s prove Leftpad with interest. However: I know Donald Knuth’s famous quote: “Beware of bugs in the above code; I have only proved it correct, not tried it” I also know how it turned out that code that had been proved correct harboured a bug not found for decades. So I thought I’d take a peek and do some testing on these Leftpad implementations that are all “provably correct”. Contents Methodology Impleme...