趁着半夜脑袋不清醒感觉问两个问题，这是第二个，写完就觉得问的有点蠢但还是发出来。
++++
几乎所有人都同意现代编程语言应该有一个类型系统，它可以限制错误的发生，但一个类型系统限制到什么程度，很难统一。
我们都知道在柯霍同构下，program=proof，也因此如果从自动定理证明器导出程序，如果自动定理证明器的搜索证明能力比较强，人只需要去给出粒度大一点的证明步骤，证明器来填充细节。
那么这里的想法是，是不是也可能从人的角度说只给出粗粒度的类型，由证明器或者类似的自动编程器给出更细粒度的type在局部使用，人只要理解和设计在big-step意义上的函数需要的type？