Muy contento con el progreso en HVM4. SupGen ahora está integrado, y finalmente tenemos un sistema de tipos nativo, funcionando directamente en redes de interacción, lo que significa que HVM será utilizable como un verificador de pruebas rápido y paralelo. No me sorprendería si termina siendo OOMs más rápido que Lean, y me gustaría aplicarlo a la demostración de teoremas RL. Además, la codificación de AI está haciendo que C sea sorprendentemente viable. La base de código de HVM ahora es 100% C - analizador, evaluador, verificador, todo - y todavía tengo el control total sobre ella. Cuando crece demasiado, paso los siguientes varios prompts solo para pulir y mejorar la calidad del código. Eso es muy importante para mantenerlo bajo control. Viniendo de Haskell, aprecio lo estable y rápido que es todo en C (¡y finalmente poder usar el 100% de mi CPU por una vez!).