Muito feliz com o progresso no HVM4. O SupGen agora está embutido e (finalmente) temos um sistema de tipo integrado, o que significa que o HVM funcionará como um verificador de prova paralelo super rápido. Eu não ficaria surpreso se acabasse sendo OOMs mais rápidos do que Lean, e acho que isso poderia ser útil ao construir ambientes de RL de prova de teoremas. Além disso: estou apaixonado por C novamente. Tudo é C agora, até mesmo o analisador. Quando a base de código cresce muito rápido, passo os próximos prompts apenas para polir e melhorar a qualidade do código. Isso mantém a base de código sob controle. Vindo de Haskell, aprecio o quão estável e rápido tudo é. Talvez não estejamos tão longe de momentos em que escrever aplicativos da web em C se torne realmente viável