Автор протестировал "доказуемо корректные" реализации функции leftpad на различных входных данных, включая символы Unicode и символы с диакритическими знаками. Цель состояла в том, чтобы выяснить, будут ли эти формально проверенные реализации соответствовать ожидаемым автором выходным данным. Методология включала выбор случайных входных данных и ручное определение желаемого вывода.Среди протестированных реализаций были Liquid Haskell, Java, Lean4 и Rust. Для сравнения также была включена реализация на Swift, "сгенерированная на слух" ChatGPT. Настройка и запуск некоторых из этих реализаций оказались сложными из-за различий в том, как они обрабатывали строковые входные данные.Результаты выявили значительные расхождения между реализациями и ожиданиями автора, при этом Rust показал особенно плохие результаты. Несколько реализаций не смогли правильно дополнить входные данные, содержащие сложные символы Unicode или символы, образованные путем объединения нескольких кодовых точек. Автор отмечает, что даже среди "доказуемо корректных" реализаций только один вход (résumé) был обработан правильно всеми, кроме Rust.Суть проблемы заключается в определении "символа" и в том, как языки программирования обрабатывают строки. Unicode определяет кодовые точки, но они не всегда напрямую соответствуют тому, что пользователь воспринимает как один символ. Такие понятия, как комбинируемые символы и различные представления Unicode (предварительно составленные или разложенные), добавляют сложности.Кроме того, разные языки программирования используют различные внутренние представления строк и абстракции. Языки, такие как Java и Javascript, используют UTF-16, что может привести к проблемам при встрече с кодовыми точками за пределами Основной многоязычной плоскости. Haskell, Lean и Python обычно рассматривают строки как последовательности кодовых точек.Строки Rust представляют собой кодовые точки, закодированные в UTF-8, а Swift абстрагирует строки до воспринимаемых пользователем символов. Эти различия в обработке Unicode и внутренних представлениях объясняют, почему реализации leftpad дали разные результаты. Автор приходит к выводу, что сложности возникают из-за неоднозначности "длины символа" и разнообразных способов реализации обработки строк в языках программирования.