Breaking "provably correct" Leftpad

Summary

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: So I thought I’d take a peek and do some testing on these Leftpad implementations that are all “provably correct”. Contents 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 for some reason I’ve made a mistake, all the implementations will at least match each other. [narrator: More lies] They’ve all been proved correct, right? Here are my inputs and expected outputs. I’m going to pad to a length of 10, and use - as padding so it can be seen and counted more easily than spaces. 1 𝄞 1 9 ---------𝄞 2 Å 1 9 ---------Å 3 𓀾 1 9 ---------𓀾 4 אֳֽ֑ 1 9 ---------אֳֽ֑ 5 résumé 6 4 ----résumé 6 résumé 6 4 ----résumé [“ordinary”, “random” - I think my work here is done…] I’ve used a monospace font so that the right hand side of the outputs all line up as you’d expect. Entry 6 is not a mistake, by the way, it just does “e acute” in a different way to entry 5. Nothing to see here, move along… Not all of the implementations were that easy to run. In fact, many of them didn’t take any kind of “string” as input, but vectors or lists or such things, and it wasn’t obvious to me how to pass strings in. So I discounted them. For the ones I could run, I attempted to do so by embedding the test inputs directly in the program, if possible. Embedding the characters directly in Haskell source code kept getting me “lexical error in string/character literal”, so I wrote a small driver program that read from a file. The leftpad function provided didn’t take a string, but a char[]. Thankfully, it’s easy to convert from String objects, using the .toCharArray() function. So I did that. The code here had loads of extra lines reg...