一些 HOC 更新： - HVM4 大部分已完成并正在测试中。虽然仍缺少一些重要的内容，但并不紧急，因此会在后面添加。HVM4 基本上是 HVM1 的超精致版本，包括我们自那以来学到的一切。我现在相信 HVM1 的方法优于 HVM2（和 Bend），因为在交互网络评估器中，懒惰是非常重要的。HVM4 将为 Bend2 和 SupGen1 提供动力。 - SupGen1 已经 100% 完成。自去年我的帖子以来没有大的改进。我们可以非常快速地合成像 sort() 这样的函数，但组合仍然很慢。我相信对于一类可融合的函数可以大大改进，这将使一些非常酷的应用成为可能，但需要更多的研究。我们希望下个月推出 API。主要的障碍是集群，目前正在迁移到一个更稳健的位置。我们被大量的巴西官僚主义所阻碍。我们能做的并不多。如果这还不够明显，让我大声说出来：不要在巴西创建科技公司。(: - Bend2 将稍晚推出，可能在 SupGen 后大约 2 个月，也就是大约 5 月？它旨在成为像 Lean 一样的证明语言，但为真实应用和氛围编码而构建，而不是数学和论文。这可能是我写过的最亵渎的句子，这就是我认为它会很棒的原因。当然，它仍然会像 Bend1 一样并行运行，通过 HVM4 进行目标定位。 团队目前正在努力工作于 HVM4 / SupGen。与此同时，我正在短暂休息，去做另一个项目，预计一个月后会回来...