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


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

++++

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

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

那么这里的想法是,是不是也可能从人的角度说只给出粗粒度的类型,由证明器或者类似的自动编程器给出更细粒度的type在局部使用,人只要理解和设计在big-step意义上的函数需要的type?

https://weibo.com/1655747731/N3OiYfN9V?pagetype=groupfeed