对HVM4的进展感到非常高兴。SupGen现在是内置的，我们终于有了一个原生类型系统，直接在交互网运行，这意味着HVM将可用作快速的并行证明验证器。我不会感到惊讶，如果它最终比Lean快几个数量级，我想将其应用于定理证明的强化学习。 此外，AI编码使得C语言变得出乎意料的可行。HVM的代码库现在是100%用C编写的——解析器、评估器、检查器，所有一切——而我仍然完全掌控它。当它增长得太多时，我会花接下来的几个提示来打磨和提高代码质量。这对保持它的稳定性非常重要。来自Haskell的我，欣赏C语言中一切的稳定性和速度（终于能够充分利用我的CPU了！）