Muy contento con el progreso en HVM4. SupGen ahora está incorporado, y finalmente tenemos un sistema de tipo nativo, que se ejecuta directamente en redes de interacción, lo que significa que HVM se podrá utilizar como un verificador de prueba rápido y paralelo. No me sorprendería si termina siendo OOM más rápido que Lean, y me gustaría aplicarlo a la demostración de teoremas RL Además, la codificación de IA 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, dedico las siguientes indicaciones 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!)