著者は、左パディング関数（leftpad function）の「証明可能な正しさ」を持つ実装を、Unicode文字やダイアクリティカルマーク付き文字を含む様々な入力に対してテストしました。その目的は、形式的に検証されたこれらの実装が、著者の期待する出力と一致するかどうかを確認することでした。手法としては、ランダムな入力を選択し、手動で期待される出力を決定しました。テストされた実装には、Liquid Haskell、Java、Lean4、Rustが含まれていました。比較のために、ChatGPTによって生成された「感覚的にコーディングされた」Swift実装も含まれていました。これらの実装の一部は、文字列入力を扱う方法の違いから、セットアップと実行が困難であることが判明しました。結果として、実装と著者の期待との間に顕著な不一致が見られ、特にRustのパフォーマンスは悪かったです。複数の実装は、複雑なUnicode文字や複数のコードポイントを組み合わせた文字を含む入力を正しくパディングできませんでした。著者は、「証明可能な正しさ」を持つ実装の間でさえ、Rustを除くすべてで正しく処理された入力は「résumé」の1つだけだったと指摘しています。問題の核心は、「文字」の定義と、プログラミング言語が文字列をどのように扱うかという点にあります。Unicodeはコードポイントを定義しますが、これらは常にユーザーが単一の文字として認識するものと直接一致するわけではありません。結合文字や異なるUnicode表現（プリコンポーズドまたはデコンポーズド）といった概念が複雑さを増します。さらに、異なるプログラミング言語は、様々な内部文字列表現と抽象化を採用しています。JavaやJavaScriptのような言語はUTF-16を使用しており、基本多言語面（Basic Multilingual Plane）以外のコードポイントに遭遇した場合に問題を引き起こす可能性があります。Haskell、Lean、Pythonは一般的に文字列をコードポイントのシーケンスとして扱います。Rustの文字列はUTF-8エンコードされたコードポイントであり、Swiftは文字列をユーザーが認識する文字に抽象化します。Unicodeの扱い方や内部表現におけるこれらの違いが、leftpadの実装が異なる出力を生成した理由を説明しています。「文字数」の曖昧さと、プログラミング言語が文字列処理を実装する多様な方法から、複雑さが生じると著者は結論付けています。