Muito feliz com o progresso no HVM4. O SupGen agora está integrado, e nós (finalmente) temos um sistema de tipos integrado, o que significa que o HVM funcionará como um verificador de provas super rápido e paralelo. Não ficaria surpreso se ele acabar sendo OOMs mais rápido que o Lean, e acho que isso pode ser útil ao construir ambientes de RL para prova de teoremas. Além disso: estou apaixonado por C novamente. Tudo agora é C, até o parser. Quando a base de código cresce rápido demais, passo os próximos vários 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 tempos em que escrever aplicativos web em C se torne realmente viável.