Breaking "provably correct" Leftpad(lukeplant.me.uk)
lukeplant.me.uk
Breaking "provably correct" Leftpad
https://lukeplant.me.uk/blog/posts/breaking-provably-correct-leftpad/
22 comments
Every time I hear people talking about ensuring software correctness, it reminds me of this story: https://horningtales.blogspot.com/2006/09/exhaustive-testing...
A university group in the 1960s finds a vendor-supplied binary-to-BCD conversion function sometimes produces an off-by-one error.
They devise a simple fix - but find it adds an extra 'drum revolution' and so write an even more refined fix, that produces the right answer without taking any extra time.
Then they test it, over the course of several weeks, counting from 0 to 9,999,999, both in binary and in BCD, converting the binary to BCD, and comparing the results.
They proudly send the perfected implementation to the vendor - who sends it on to other users of the machine. Soon after they receive a phone call: "Were you aware that your new routine drops the sign of negative numbers?"
A university group in the 1960s finds a vendor-supplied binary-to-BCD conversion function sometimes produces an off-by-one error.
They devise a simple fix - but find it adds an extra 'drum revolution' and so write an even more refined fix, that produces the right answer without taking any extra time.
Then they test it, over the course of several weeks, counting from 0 to 9,999,999, both in binary and in BCD, converting the binary to BCD, and comparing the results.
They proudly send the perfected implementation to the vendor - who sends it on to other users of the machine. Soon after they receive a phone call: "Were you aware that your new routine drops the sign of negative numbers?"
When I was an intern in the mid-80s we were cross-compiling for a 68000-based device (on a VAX, no less) but had our own version of the C library, supposedly because of some legal issues with the compiler vendor.
Part of this library was the routine to divide 32-bit integers, since the only native divide was 16x16 -> 32. Our implementation was the textbook shift-and-subtract algorithm, which took something like 1000 cycles on that CPU. Our routing algorithm did enough division that this ended up being a big deal, so they asked their intern to optimize it.
I came up with a version using the hardware instruction that was maybe 5-10x faster; they tested it a bit and sent a software update out to customers, after which the "phone home" monitoring (using real phone lines and modems in those days) started blowing up.
If you divide by zero, naive shift-and-subtract will return MAXINT, while the hardware instruction will raise a divide-by-zero exception. On startup we had a bunch of averages that were default-initialized to zero, and we'd divide by some of them. Getting 32-bit MAXINT wasn't a really big deal - it put a big spike into some moving averages, which decayed pretty quickly. An unexpected exception, though, was a big problem...
Part of this library was the routine to divide 32-bit integers, since the only native divide was 16x16 -> 32. Our implementation was the textbook shift-and-subtract algorithm, which took something like 1000 cycles on that CPU. Our routing algorithm did enough division that this ended up being a big deal, so they asked their intern to optimize it.
I came up with a version using the hardware instruction that was maybe 5-10x faster; they tested it a bit and sent a software update out to customers, after which the "phone home" monitoring (using real phone lines and modems in those days) started blowing up.
If you divide by zero, naive shift-and-subtract will return MAXINT, while the hardware instruction will raise a divide-by-zero exception. On startup we had a bunch of averages that were default-initialized to zero, and we'd divide by some of them. Getting 32-bit MAXINT wasn't a really big deal - it put a big spike into some moving averages, which decayed pretty quickly. An unexpected exception, though, was a big problem...
The “random” choice of swift was quite fortunate since what this really seems to be testing is the ergonomics of the Unicode “character” definition in the standard libraries used, and swift has the best defaults of the languages mentioned haha
> Swift’s string implementation goes to heroic efforts to be as Unicode-correct as possible. […] This is great for correctness, but it comes at a price, mostly in terms of unfamiliarity; if you’re used to manipulating strings with integer indices in other languages, Swift’s design will seem unwieldy at first, leaving you wondering.
> It’s not that other languages don’t have Unicode-correct APIs at all — most do. For instance, NSString has the enumerateSubstrings method that can be used to walk through a string by grapheme clusters. But defaults matter; Swift’s priority is to do the correct thing by default.
> Strings in Swift are very different than their counterparts in almost all other mainstream programming languages. When you’re used to strings effectively being arrays of code units, it’ll take a while to switch your mindset to Swift’s approach of prioritizing Unicode correctness over simplicity.
> Ultimately, we think Swift makes the right choice. Unicode text is much more complicated than what those other languages pretend it is. In the long run, the time savings from avoided bugs you’d otherwise have written will probably outweigh the time it takes to unlearn integer indexing.
— https://oleb.net/blog/2017/11/swift-4-strings/
> It’s not that other languages don’t have Unicode-correct APIs at all — most do. For instance, NSString has the enumerateSubstrings method that can be used to walk through a string by grapheme clusters. But defaults matter; Swift’s priority is to do the correct thing by default.
> Strings in Swift are very different than their counterparts in almost all other mainstream programming languages. When you’re used to strings effectively being arrays of code units, it’ll take a while to switch your mindset to Swift’s approach of prioritizing Unicode correctness over simplicity.
> Ultimately, we think Swift makes the right choice. Unicode text is much more complicated than what those other languages pretend it is. In the long run, the time savings from avoided bugs you’d otherwise have written will probably outweigh the time it takes to unlearn integer indexing.
— https://oleb.net/blog/2017/11/swift-4-strings/
The author explicitly notes
> The Swift implementation was indeed written by ChatGPT, and it got it right first time, with just the prompt “Implement leftpad in Swift”. However: Swift is the only language I know where an implementation that does what I wanted it to do is that simple.
> The Swift implementation was indeed written by ChatGPT, and it got it right first time, with just the prompt “Implement leftpad in Swift”. However: Swift is the only language I know where an implementation that does what I wanted it to do is that simple.
Reading between the lines that definitely seems like an intentional choice
> swift has the best defaults
Not really. Swift's defaults happens to match best to these particular requirements. Change the task and you will find other languages have the "best" defaults.
Not really. Swift's defaults happens to match best to these particular requirements. Change the task and you will find other languages have the "best" defaults.
Hillel Wayne posted a followup https://buttondown.com/hillelwayne/archive/three-ways-formal... which may be interesting. Essentially the issue is "what does the Length of a string mean?"
> The leftpad function provided[1] 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.
Java's unicode handling is a monumental footgun of the most devastating variety where it works for most common cases, and almost all code that is not written with care to how it is handled will not deal well with code points that require more than 2 bytes to represent.
If you insist on using a char array (which is a bit unidiomatic), you should be using Character$charPointCount[2] to figure out how many code points are in the array, and even then you're probably SOL with regards to non-trivial emojis. String$charPointCount[3] is also an option if you want to use String and StringBuilder to do the padding, which arguably be more idiomatic.
[1] https://github.com/hwayne/lets-prove-leftpad/blob/ea9c0f09a2...
[2] https://docs.oracle.com/en/java/javase/25/docs/api//java.bas...
[3] https://docs.oracle.com/en/java/javase/25/docs/api//java.bas...
Java's unicode handling is a monumental footgun of the most devastating variety where it works for most common cases, and almost all code that is not written with care to how it is handled will not deal well with code points that require more than 2 bytes to represent.
If you insist on using a char array (which is a bit unidiomatic), you should be using Character$charPointCount[2] to figure out how many code points are in the array, and even then you're probably SOL with regards to non-trivial emojis. String$charPointCount[3] is also an option if you want to use String and StringBuilder to do the padding, which arguably be more idiomatic.
[1] https://github.com/hwayne/lets-prove-leftpad/blob/ea9c0f09a2...
[2] https://docs.oracle.com/en/java/javase/25/docs/api//java.bas...
[3] https://docs.oracle.com/en/java/javase/25/docs/api//java.bas...
For anyone else who was curious C#/.NET:
By default string.Length measures characters, but System.Globalization.StringInfo is provided to work with "text elements".
Unlike System.String, StringInfo doesn't have a built-in PadLeft function in it's base library. But it gets the length "right" by the author's standard.
Code to show lengths:
By default string.Length measures characters, but System.Globalization.StringInfo is provided to work with "text elements".
Unlike System.String, StringInfo doesn't have a built-in PadLeft function in it's base library. But it gets the length "right" by the author's standard.
Code to show lengths:
using System;
using System.Globalization;
public class Program
{
public static void Main()
{
var weirdStrings = new string[] {"𝄞","Å","𓀾","אֳֽ֑","résumé","résumé"};
foreach(var weirdString in weirdStrings){
var asStringInfo = new StringInfo(weirdString);
Console.WriteLine($"{weirdString.PadLeft(10,'-')} {weirdString.Length} {asStringInfo.LengthInTextElements}");
}
}
}If you skimmed the article and missed the subtle notes, the author deliberately chose the wrong way to use the Rust version to make a point. Even ChatGPT told him it was wrong for his use case:
> As mentioned, the other way to use the Rust version has the same behaviour as the Haskell/Lean/etc versions. ChatGPT did actually point out to me that this way was better, and the other way (the one I used) was adequate only if the input was limited to ASCII.
> As mentioned, the other way to use the Rust version has the same behaviour as the Haskell/Lean/etc versions. ChatGPT did actually point out to me that this way was better, and the other way (the one I used) was adequate only if the input was limited to ASCII.
Yes, there was vibe coding throughout.
Should've probably been an article about how vibe coding results in incorrect software.
Should've probably been an article about how vibe coding results in incorrect software.
It’s more than that. ChatGPT actually gave the right answer but they chose not to use it to make a point.
Not quite right... as there would still be 3 failures in the tests, like Haskel.
Realistically, I would expect to have a couple different methods available... one that split a string into groups of code segments that represent a single unit, and a display width of units (0-2). Alternatively another method that just counted the display width in numbers of character spaces (assuming mono-spacing). Then you could apply the padding more naturally.
The grouping of characters would be more for other tests for display beyond left padding.
Realistically, I would expect to have a couple different methods available... one that split a string into groups of code segments that represent a single unit, and a display width of units (0-2). Alternatively another method that just counted the display width in numbers of character spaces (assuming mono-spacing). Then you could apply the padding more naturally.
The grouping of characters would be more for other tests for display beyond left padding.
Found it... Counting display width[1], getting unicode segments[2].
1. https://crates.io/crates/unicode-display-width
2. https://crates.io/crates/unicode-segmentationThey were definitely trying to make Rust look worse than it is. They even sarcastically acknowledge that:
> I didn’t deliberately pick the one which made Rust look even worse than all the others, out of peevish resentment for every time someone has rewritten some Python code (my go-to language) in Rust and made it a million times faster – that’s a ridiculous suggestion.
And
> Rust, as expected, gets nul points. What can I say?
> I didn’t deliberately pick the one which made Rust look even worse than all the others, out of peevish resentment for every time someone has rewritten some Python code (my go-to language) in Rust and made it a million times faster – that’s a ridiculous suggestion.
And
> Rust, as expected, gets nul points. What can I say?
To be fair, you'd have to also import this crate to get the result he wanted:
https://docs.rs/unicode-segmentation/latest/unicode_segmenta...
https://docs.rs/unicode-segmentation/latest/unicode_segmenta...
What is the expected output of padding "﷽"? It is only one code point but very wide.
There is a definition file on unicode spec about a character should be n half-width in monospacr context. Not sure if it includes all symbol though. Also don't know if it handles symbol that has more than 2 half-width
https://www.unicode.org/reports/tr11/
https://www.unicode.org/reports/tr11/
Further reading on the Knuth correctness quote
https://staff.fnwi.uva.nl/p.vanemdeboas/knuthnote.pdf
I think to get it right, leftpad will have to link to libghostty :)
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.