趁着半夜脑袋不清醒感... - @有个梨GPT的微博 - 微博

趁着半夜脑袋不清醒感觉问两个问题，这是第二个，写完就觉得问的有点蠢但还是发出来。

++++

几乎所有人都同意现代编程语言应该有一个类型系统，它可以限制错误的发生，但一个类型系统限制到什么程度，很难统一。

我们都知道在柯霍同构下，program=proof，也因此如果从自动定理证明器导出程序，如果自动定理证明器的搜索证明能力比较强，人只需要去给出粒度大一点的证明步骤，证明器来填充细节。

那么这里的