L'auteur a testé des implémentations "prouvablement correctes" de la fonction leftpad avec diverses entrées, y compris des caractères Unicode et des caractères avec des diacritiques. L'objectif était de voir si ces implémentations formellement vérifiées correspondraient aux sorties attendues par l'auteur. La méthodologie impliquait la sélection d'entrées aléatoires et la détermination manuelle de la sortie souhaitée.Les implémentations testées comprenaient Liquid Haskell, Java, Lean4 et Rust. À titre de comparaison, une implémentation Swift "codée à l'instinct" générée par ChatGPT a également été incluse. La mise en place et l'exécution de certaines de ces implémentations se sont avérées difficiles en raison des différences dans la manière dont elles traitaient les entrées de chaînes de caractères.Les résultats ont révélé des divergences importantes entre les implémentations et les attentes de l'auteur, Rust étant particulièrement performant. Plusieurs implémentations n'ont pas réussi à compléter correctement les entrées contenant des caractères Unicode complexes ou des caractères formés par la combinaison de plusieurs points de code. L'auteur note que même parmi les implémentations "prouvablement correctes", une seule entrée (résumé) a été traitée correctement par toutes, à l'exception de Rust.Le cœur du problème réside dans la définition d'un "caractère" et la manière dont les langages de programmation gèrent les chaînes de caractères. Unicode définit des points de code, mais ceux-ci ne correspondent pas toujours directement à ce qu'un utilisateur perçoit comme un seul caractère. Des concepts tels que les caractères combinés et les différentes représentations Unicode (pré-composées ou décomposées) ajoutent de la complexité.De plus, différents langages de programmation utilisent des représentations et des abstractions de chaînes de caractères internes variées. Des langages comme Java et Javascript utilisent UTF-16, ce qui peut entraîner des problèmes lorsque des points de code en dehors du Basic Multilingual Plane sont rencontrés. Haskell, Lean et Python traitent généralement les chaînes de caractères comme des séquences de points de code.Les chaînes de caractères Rust sont des points de code encodés en UTF-8, et Swift abstrait les chaînes de caractères en caractères perçus par l'utilisateur. Ces différences dans la gestion de l'Unicode et des représentations internes expliquent pourquoi les implémentations de leftpad ont produit des sorties différentes. L'auteur conclut que les complexités proviennent de l'ambiguïté de la "longueur de caractère" et des diverses manières dont les langages de programmation implémentent la gestion des chaînes de caractères.