So it's not really leftpad that's broken, it's that each language has a different definition of "String.length", generally corresponding to the definition of th

So it's not really leftpad that's broken, it's that each language has a different definition of "String.length", generally corresponding to the definition of the underlying encoding, when dealing with accents, emojis, foreign characters, etc., and which notably does not always correspond to the number of spaces occupied by a string a monospace font. IOW the proofs are correct: leftpad will result in spaces on the left, input string on the right, and String.length as specified. It's the spec itself that was incorrect: the last requirement should be based on "number of spaces occupied by the string in a monospace font", not "string.length", if that's what the desired requirement is. That said, I think that's largely the author's point. You can prove that your code meets the spec, but you can't prove that your spec meets what you actually intended.