对HVM4的进展感到非常高兴。SupGen现在已经内置，我们（终于）有了一个集成的类型系统，这意味着HVM将双重作为一个超级快速的并行证明验证器。我不会感到惊讶，如果它最终比Lean快几个数量级，我认为这在构建定理证明强化学习环境时会很有用。 另外：我又爱上了C。现在一切都是C，甚至解析器。当代码库增长得太快时，我会花接下来的几个提示来打磨和提高代码质量。这保持了代码库的稳定性。来自Haskell的我，欣赏一切是多么稳定和快速。也许我们离用C编写Web应用程序的时代并不遥远，实际上是可行的。