Très heureux des progrès sur HVM4. SupGen est maintenant intégré, et nous avons (enfin) un système de types intégré, ce qui signifie que HVM fera également office de vérificateur de preuves super rapide et parallèle. Je ne serais pas surpris s'il s'avérait être des OOMs plus rapide que Lean, et je pense que cela pourrait être utile lors de la construction d'environnements de preuve de théorèmes en RL. Aussi : je suis de nouveau amoureux de C. Tout est C maintenant, même le parseur. Lorsque la base de code croît trop vite, je passe les prochaines invites juste à peaufiner et améliorer la qualité du code. Cela permet de garder la base de code sous contrôle. Venant de Haskell, j'apprécie à quel point tout est stable et rapide. Peut-être ne sommes-nous pas si loin des temps où écrire des applications web en C devient réellement viable.