Breaking “provably correct” Leftpad
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”. Methodology I’ll pick a few, simple, perfectly ordinary inputs at random, and work out what I think the output should be. This is a pretty trivial problem so I’m expecting that all the implementations will match my output. [narrator: He is is expecting no such thing] I’m also expecting that, even if…
