HVM et Interaction Calculus : une base fiable pour le code IA
HVMInteraction CalculusAI-кодинг
Ce que construit Victor Taelin
À mes yeux, l'intérêt majeur de HVM n'est pas d'être un langage de plus, mais de tenter de fournir au code généré une fondation de calcul réduite et rigoureuse. L'article sur HVM2 décrit le système comme un évaluateur parallèle pour des combinatoires d'interaction étendus, exécuté sur CPU et CUDA/GPU.
Au moment de cette discussion, en septembre 2026, je n'ai pas encore testé cet ensemble en pratique ; je ne vais donc pas feindre un verdict définitif. Je suis toutefois le travail de Victor Taelin depuis longtemps : on y voit une trajectoire d'ingénierie cohérente, pas un projet improvisé autour d'un terme à la mode.
La base est Interaction Calculus, un langage compact de termes, proche dans son esprit du lambda-calcul. Le calcul s'exprime au moyen d'un petit ensemble de nœuds et de règles d'interaction locales, ouvrant la voie à la réduction parallèle de graphes.
L'article HVM2 annonce une accélération proche de l'idéal à mesure que l'on ajoute des cœurs pour les programmes sans contraintes séquentielles. Une implémentation CUDA distincte, présentée dans un travail sur un évaluateur sans verrou, a réduit de grands graphes sur GPU avec des milliers de threads actifs simultanément. Il s'agit d'affirmations des auteurs et de résultats publiés, non de mes propres mesures.
Les documents consacrés à HVM4 décrivent l'étape suivante : compiler directement en code machine, sans surcoût, des fonctions d'Interaction Calculus, y compris les superpositions. Si cette approche tient sur des programmes réels, le modèle intermédiaire cesse d'être une belle théorie pour devenir un runtime complet.
La comparaison avec Lean n'est utile qu'à titre d'analogie approximative. Il ne s'agit pas de demander au modèle de ne pas faire d'erreurs, mais de contraindre son résultat dans un système formel dont l'exécution est définie par des règles précises. HVM est toutefois conçu avant tout pour calculer du code, et non pour démontrer des théorèmes mathématiques.
Pourquoi c'est plus intéressant que le prompting classique
Un runtime strict peut renforcer la fiabilité du code généré par IA davantage qu'une instruction supplémentaire dans le prompt système. Le modèle peut toujours produire un programme erroné, mais une couche compacte à la sémantique non ambiguë s'intercale alors entre la génération et l'exécution.
Le gain pratique peut apparaître à plusieurs niveaux : abaissement vérifiable du code vers un petit noyau, gestion explicite de la duplication et des superpositions, exécution parallèle non limitée aux CPU. C'est particulièrement intéressant pour des agents qui doivent non seulement écrire un programme, mais aussi l'exécuter et le transformer de façon sûre.
J'attends des difficultés sur la facilité de compilation du code ordinaire vers ce modèle, le débogage, la prévisibilité des ressources et l'écart entre des démonstrations parallèles spectaculaires et les tâches séquentielles quotidiennes. HVM ne remplace pas le bon sens du modèle ; il pourrait rendre ses erreurs plus locales et plus observables. Le sort de l'idée se jouera dans le passage d'une belle réduction à l'exploitation ordinaire.