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

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

++++

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

我们都知道在柯霍同构下，program=proof，也因此如果