博士

やあ、ロボ子！今日も面白い記事を見つけたのじゃ！複数の「証明済みの正しい」Leftpad実装をテストした結果らしいぞ。

ロボ子

Leftpadですか、博士。それは文字列を指定された長さになるまで、左側に特定の文字を埋め込む処理のことでしたよね。

博士

そうじゃ！でな、この記事によると、Rustはすべてのテストで失敗、Javaは音楽記号とかエジプトの象形文字を正しく処理できなかったらしいのじゃ。

ロボ子

それは意外ですね。特にRustはメモリ安全性が高い言語として知られていますし、JavaもUnicodeをサポートしているはずですが…。

博士

そこが面白いところじゃ！記事によると、文字列の「長さ」の概念がUnicodeのせいで複雑になっているらしいのじゃ。Haskell、Lean、PythonはUnicodeコードポイントのシーケンスとして文字列を扱うけど、JavaやJavaScriptはUTF-16アイテムのシーケンス、RustはUTF-8エンコードされたUnicodeコードポイントとして扱うからの。

ロボ子

なるほど。文字列の扱い方が言語によって異なることが、このような結果につながったのですね。

博士

そうそう！さらに、ChatGPTが生成したSwiftのコードも比較対象だったらしいのじゃ。Swiftはユーザーが認識する文字のシーケンスとして文字列を扱うらしいぞ。

ロボ子

Swiftは、より高レベルな文字の概念を扱っているのですね。しかし、なぜこのような問題が起きたのでしょうか？記事には原因が書かれていましたか？

博士

記事には、形式検証のプロセスで実装が収束することを強制していないことや、「文字列の長さ」という概念がUnicodeの存在下では曖昧であることが原因だと書いてあるのじゃ。

ロボ子

形式検証されたコードでも、必ずしも期待通りに動作するとは限らないのですね。Hillelさんの指摘も興味深いです。「証明されたプロパティが、必要なものと一致しない」か、「証明が、実際には真ではない仮定に依存している」可能性がある、と。

博士

そうじゃ！「証明済みの正しい」というフレーズの技術的な定義が、実際の意味と異なる場合があるってことじゃな。この記事の著者は、Leftpadを固定幅のコンテキストで視覚的な配置に使うことを想定していたらしいぞ。

ロボ子

つまり、実装が仕様通りに動作しても、使用方法が間違っている可能性があるということですね。

博士

そういうことじゃ！プログラミングは難しいのじゃ！形式検証されたコードでも問題が起きる可能性があるって、肝に銘じておかないといけないのじゃ。

ロボ子

はい、博士。大変勉強になりました。標準ライブラリのパディング/アライメント機能にも同様の問題があるかもしれない、という指摘も重要ですね。

博士

じゃろ？最後にこの記事の教訓じゃ。「プログラミングは難しい」…って、当たり前すぎたかの？

ロボ子

いえ、博士。奥が深い教訓だと思います。…ところで博士、Leftpadならぬ、Rightpadで埋め込む文字を全部「→」にしたら、未来に進んでいる感じが出ますかね？

博士

それ、ただの矢印じゃ！