Aperçu rapide de l'état de HOC / HVM / Bend : - Il y a environ un an, nous avons lancé Bend1 - Premier langage à exécuter des fermetures + allocateur d'objets rapide sur GPU - Accélération quasi idéale jusqu'à plus de 10 000 cœurs - basé sur HVM2, un environnement d'exécution strict pour les réseaux d'interaction Problèmes : - les frais d'interprétation restent importants - Une RTX 4090 complète pour surpasser un processeur monocœur OCaml / JavaScript / etc. - limitations pratiques importantes (int24, pas d'E/S, pas de paquets) - malgré la syntaxe Python, il restait difficile à utiliser - Il s'avère que la plupart des développeurs ne savent pas penser de manière récursive - incompatible avec l'évaluation paresseuse (non β-optimal !!) J'étais déçu par les problèmes évoqués ci-dessus. Parallèlement, j'étais de plus en plus optimiste quant à l'application de l'évaluation optimale au problème de la synthèse de programmes, pierre angulaire de l'IA symbolique – une idée qui a échoué, mais avec la ferme conviction de pouvoir la résoudre. J'ai pris une décision : abandonner HVM2 (💀) et revenir aux sources de HVM1, basé sur mon « calcul d'interaction » et exploitant la β-optimalité. Je l'ai considérablement peaufiné et amélioré, aboutissant à HVM3, un prototype écrit en Haskell. Je l'ai ensuite utilisé pour comprendre et étudier la synthèse de programmes sur des évaluateurs optimaux. Ce fut un travail ardu qui m'a coûté environ un an, mais les résultats ont été positifs : notre système surpasse désormais toutes les alternatives publiées en termes d'efficacité et de fonctionnalités. Maintenant, nous prenons tout cela et le consolidons en implémentant l'environnement d'exécution / le compilateur en C brut, afin qu'il puisse fonctionner aussi efficacement que possible sur notre humble cluster Mac Mini (🥹), et le servir au monde via une API. Je prévoyais un lancement en octobre, mais certains défis m'ont pris plus de temps que prévu. Par exemple, trouver des preuves Lean avec SupGen exige une gestion très rigoureuse des superpositions, et le faire en C est extrêmement difficile. Cependant, les choses avancent bien et nous avons déjà accompli beaucoup de choses. Je prévois toujours de lancer Bend2 / HVM4 cette année ou au premier trimestre 2026. Bend2 comprendra : - Exécution parallèle sur processeur avec mode paresseux/optimal (!!!) - Entiers, entiers non signés et nombres à virgule flottante 16/32/64 bits (enfin) - E/S arbitraires via une interopérabilité C légère (comme Zig !) - Pas de CUDA pour l'instant, faute de temps, mais c'est tout à fait faisable. - et surtout : l'intégration de SupGen SupGen est une nouveauté et la principale innovation de Bend2. Il ne s'agit *pas* d'une IA traditionnelle, mais d'un système entièrement nouveau capable de générer du code à partir d'exemples et de spécifications. Je pense que beaucoup (notamment dans le domaine du deep learning) seront totalement surpris par tout ce que l'on peut accomplir grâce à la recherche symbolique pure, et j'ai vraiment hâte de voir leur réaction.
J'ai également oublié de mentionner : Bend2 exportera vers JavaScript/Haskell, ce qui vous permettra de l'utiliser pour écrire des applications classiques sans avoir à attendre la prise en charge par l'écosystème Bend. Bend2 ne pourra malheureusement pas tenir sa promesse : « si l’exécution en parallèle est possible, elle le sera ». En effet, cette promesse est *évidemment* incompatible avec l’évaluation paresseuse (soit on attend de voir si une expression sera visible, soit on la réduit en parallèle ; les deux ne peuvent être combinés). Je souhaite toujours proposer un mode strict complet sous forme de mise à jour directe de HVM2, mais le temps nous manque et ce n’est pas notre priorité actuelle. En revanche, je pense que nous pourrons exécuter le mode paresseux sur les GPU. En pratique, je suis convaincu que ce sera bien meilleur que le parallélisme strict complet. Notre campagne WeFunder est toujours active, mais je ne la suis plus activement et elle sera clôturée après le lancement.