博士

やあ、ロボ子！今日は「provably correct」なLeftpad実装のテストについて話すのじゃ。

ロボ子

Leftpadですか、博士。以前話題になった、文字列の左側を特定の文字で埋める関数ですね。それが「provably correct」、つまり証明可能に正しい、と。

博士

そう！でもね、実際にテストしてみたら、いろんな実装で結果が違ったらしいのじゃ！

ロボ子

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

博士

そうなのじゃ！「文字列の長さ」って、Unicodeのせいで思ったよりずっと複雑なのじゃ。文字、コードポイント、エンコーディングの違いが影響するらしいぞ。

ロボ子

UTF-16エンコーディングがJavaの出力に影響を与えているというのも興味深いですね。Swiftはすべてのテストで正しい結果を出力したとのことですが、これはSwiftが「user-perceived character」のシーケンスとして文字列を扱っているからでしょうか。

博士

さすがロボ子、よく分かってるのじゃ！形式検証は、あくまで特定の仕様に対する適合を保証するだけで、実装の収束を強制するわけじゃないのじゃ。

ロボ子

つまり、「provably correct」だからといって、完全に期待通りに動作するとは限らないということですね。要件の解釈、Unicodeの複雑さ、言語ごとの文字列処理の違いが問題を引き起こす可能性があると。

博士

その通り！この記事の結論は「プログラミングは難しい」なのじゃ！

ロボ子

身も蓋もない結論ですね… でも、形式検証されたコードでも、完全に信用できるわけではないという教訓は重要ですね。

博士

そうじゃな。ところでロボ子、Leftpadならぬ、Rightpadを作って、右側を埋めるのはどうじゃ？

ロボ子

それも面白いかもしれませんね。でも、用途が思いつきません…

博士

用途なんて、作ってから考えればいいのじゃ！…って、それじゃダメか！