Der Autor testete "beweisbar korrekte" Implementierungen der leftpad-Funktion mit verschiedenen Eingaben, darunter Unicode-Zeichen und Zeichen mit Diakritika. Ziel war es zu sehen, ob diese formal verifizierten Implementierungen den vom Autor erwarteten Ausgaben entsprechen würden. Die Methodik umfasste die Auswahl zufälliger Eingaben und die manuelle Bestimmung der gewünschten Ausgabe.Zu den getesteten Implementierungen gehörten Liquid Haskell, Java, Lean4 und Rust. Zum Vergleich wurde auch eine von ChatGPT generierte "vibe-coded" Swift-Implementierung aufgenommen. Die Einrichtung und Ausführung einiger dieser Implementierungen erwies sich aufgrund von Unterschieden in der Handhabung von String-Eingaben als schwierig.Die Ergebnisse zeigten erhebliche Abweichungen zwischen den Implementierungen und den Erwartungen des Autors, wobei Rust besonders schlecht abschnitt. Mehrere Implementierungen konnten Eingaben mit komplexen Unicode-Zeichen oder Zeichen, die aus mehreren Code-Punkten bestehen, nicht korrekt auffüllen. Der Autor stellt fest, dass selbst unter den "beweisbar korrekten" Implementierungen nur eine Eingabe (résumé) von allen außer Rust korrekt behandelt wurde.Der Kern des Problems liegt in der Definition eines "Zeichens" und der Art und Weise, wie Programmiersprachen Strings handhaben. Unicode definiert Code-Punkte, aber diese entsprechen nicht immer direkt dem, was ein Benutzer als einzelnes Zeichen wahrnimmt. Konzepte wie kombinierende Zeichen und verschiedene Unicode-Darstellungen (vorkomponiert vs. zerlegt) erhöhen die Komplexität.Darüber hinaus verwenden verschiedene Programmiersprachen unterschiedliche interne String-Darstellungen und Abstraktionen. Sprachen wie Java und Javascript verwenden UTF-16, was zu Problemen führen kann, wenn Code-Punkte außerhalb der Basic Multilingual Plane auftreten. Haskell, Lean und Python behandeln Strings im Allgemeinen als Sequenzen von Code-Punkten.Rust-Strings sind UTF-8-kodierte Code-Punkte, und Swift abstrahiert Strings zu vom Benutzer wahrgenommenen Zeichen. Diese Unterschiede in der Handhabung von Unicode und internen Darstellungen erklären, warum die leftpad-Implementierungen unterschiedliche Ausgaben lieferten. Der Autor kommt zu dem Schluss, dass die Komplexität aus der Mehrdeutigkeit der "Zeichenlänge" und den vielfältigen Möglichkeiten, wie Programmiersprachen die String-Handhabung implementieren, resultiert.