"증명 가능한 올바른" leftpad 구현의 테스트 결과저자는 다양한 입력, 특히 유니코드 문자와 발음 구별 기호가 있는 문자를 포함하여 "증명 가능한 올바른" leftpad 함수의 구현을 테스트했습니다. 목표는 형식적으로 검증된 구현이 저자가 예상한 출력과 일치하는지 확인하는 것이었습니다. 방법론은 무작위 입력을 선택하고 수동으로 원하는 출력을 결정하는 것을 포함했습니다.테스트된 구현에는 Liquid Haskell, Java, Lean4 및 Rust가 포함되었습니다. 비교를 위해 ChatGPT에서 생성된 "vibe-coded" Swift 구현도 포함되었습니다. 일부 구현의 설정 및 실행은 문자열 입력을 처리하는 방식의 차이로 인해 어려움을 겪었습니다.결과적으로 구현과 저자의 예상 사이에 상당한 불일치가 나타났으며, 특히 Rust의 성능이 저조했습니다. 여러 구현에서 복잡한 유니코드 문자 또는 여러 코드 포인트가 결합된 문자를 포함하는 입력을 올바르게 패딩하지 못했습니다. 저자는 "증명 가능한 올바른" 구현 중에서도 Rust를 제외한 모든 구현에서 하나의 입력(résumé)만 올바르게 처리되었다고 언급합니다.문제의 핵심은 "문자"의 정의와 프로그래밍 언어가 문자열을 처리하는 방식에 있습니다. 유니코드는 코드 포인트를 정의하지만, 이는 항상 사용자가 단일 문자로 인식하는 것과 직접적으로 일치하지는 않습니다. 결합 문자 및 다양한 유니코드 표현(사전 구성 대 분해)과 같은 개념은 복잡성을 더합니다.또한, 다양한 프로그래밍 언어는 다양한 내부 문자열 표현 및 추상화를 사용합니다. Java 및 Javascript와 같은 언어는 UTF-16을 사용하며, 이는 기본 다국어 평면(Basic Multilingual Plane) 외부의 코드 포인트가 발생할 때 문제가 발생할 수 있습니다. Haskell, Lean 및 Python은 일반적으로 문자열을 코드 포인트 시퀀스로 취급합니다.Rust 문자열은 UTF-8로 인코딩된 코드 포인트이며, Swift는 문자열을 사용자가 인식하는 문자로 추상화합니다. 유니코드 및 내부 표현을 처리하는 이러한 차이는 leftpad 구현이 다른 출력을 생성한 이유를 설명합니다. 저자는 복잡성이 "문자 길이"의 모호성과 프로그래밍 언어가 문자열 처리를 구현하는 다양한 방식에서 비롯된다고 결론짓습니다.