Muy contento con el progreso en HVM4. SupGen ahora está incorporado, y (finalmente) tenemos un sistema de tipos integrado, lo que significa que HVM funcionará como un verificador de prueba paralelo súper rápido. No me sorprendería si termina siendo OOM más rápido que Lean, y creo que podría ser útil al construir entornos de RL que prueban teoremas. Además: estoy enamorado de C de nuevo. Todo es C ahora, incluso el analizador. Cuando la base de código crece demasiado rápido, dedico las siguientes indicaciones solo para pulir y mejorar la calidad del código. Esto mantiene la base de código bajo control. Viniendo de Haskell, aprecio lo estable y rápido que es todo. Quizás no estemos tan lejos de los tiempos en que escribir aplicaciones web en C se vuelve realmente viable