Contrôle douanier pour le code : comment garantir une optimisation sans faille des programmes pour enfants ✛

Un enfant assemble dans Scratch un jeu simple : le personnage apparaît au centre et saute instantanément dans un coin. Le premier déplacement disparaît entre les images — personne ne le voit. Supprimer une telle commande est sans danger. Mais comment un optimiseur automatique peut-il le savoir ? Aujourd'hui, le dépôt Scratch contient des dizaines de millions de projets écrits par de jeunes auteurs. Une erreur de l'améliorateur pourrait déformer leur intention sans qu'on s'en aperçoive.

La solution évoque un contrôle douanier. L'optimiseur non vérifié scanne le projet, construit un graphe de dépendances et propose de supprimer, par exemple, un costume inutilisé ou une commande morte. La modification est accompagnée d'un « certificat » — une déclaration numérique précisant le type de changement et les conditions de sécurité. L'inspecteur-contrôleur de confiance, qui ne croit pas un mot de ce qui est écrit, réanalyse les deux versions du programme. Il recalcule toutes les conditions. La lentille d'observation (l'ensemble des événements visibles pour le joueur) sert de repère principal : si une écriture dans une ressource est écrasée avant d'être observable, on peut la supprimer. C'est le théorème central du cadre coopératif, prouvé dans Lean. Aucune ruse ne peut échapper au certificat.

L'expérience sur 300 projets réels a montré qu'au moins une amélioration sûre a été obtenue pour 283 projets, soit 94,3 %. On a surtout nettoyé les ressources inutilisées, mais dans 17 cas, on a aussi supprimé des écritures sémantiquement mortes. Le plus important : une attaque contradictoire de 4 278 modifications avec des erreurs délibérément tissées n'a jamais percé. Le contrôleur a rejeté toutes les variantes dangereuses. L'oracle différentiel, qui a comparé le comportement des programmes original et optimisé sur une machine virtuelle, n'a constaté aucune divergence.

Pour la première fois, pour un langage parallèle orienté événements, on a construit un système où chaque modification porte un certificat vérifiable. Cela transpose la discipline des compilateurs vérifiés dans un monde où le prix de l'erreur est particulièrement élevé. Le théorème du cadre coopératif est paramétré par le type de ressource et la lentille d'observation — une seule preuve couvre toute une classe d'optimisations. Il assure la complétude informationnelle des conditions de correction, en éliminant tout canal d'observation inattendu. La base de confiance est compacte : 9 921 lignes en Python et 5 909 lignes de preuves dans Lean — un volume que peut auditer une petite équipe. L'approche ne repose pas sur des hypothèses probabilistes ni sur l'inférence bayésienne : elle offre des garanties absolues. Le programme peut être considéré comme un système dynamique, et sa vérification comme une analyse déterministe, et non comme un processus stochastique.

La douane pour le code fonctionne déjà. À l'avenir, elle pourra vérifier les modifications proposées par l'intelligence artificielle et devenir la base d'assistants IA de confiance. En attendant, l'inspecteur est prêt à travailler : quand l'enfant appuiera sur « lancer », son intention restera intacte.