haskell - 依赖类型可以证明您的代码在规范范围内是正确的。但如何证明该规范是正确的呢？

Question

依赖类型经常被宣传为一种使您能够断言程序在规范范围内正确的方法。因此，例如，您被要求编写一个对列表进行排序的代码 - 您可以通过将“排序”的概念编码为类型并编写一个函数来证明代码是正确的如列出a -> SortedList a。但是如何证明 SortedList 规范是正确的呢？难道不是这样吗:您的规范越复杂，您对该规范作为类型的编码就越有可能不正确吗？

Answer 1

这是 How do you tell that your tests are correct? 的静态类型系统版本

我能诚实给出的唯一答案是，是的，你的规范越复杂和笨拙，你就越有可能犯错误。您可能会以类型论形式主义编写某些内容，就像将程序的描述形式化为可执行函数一样。

希望您的规范足够简单且足够小，可以通过检查来判断，而您的实现可能会大得多。它的帮助是，一旦你有了一些正式的“种子”想法，你就可以证明从中衍生的想法是正确的。从这个角度来看，您越容易从更简单的部分机械地、可证明地派生出规范的各个部分，并最终从规范中派生出您的实现，您就越有可能获得正确的实现。

但是如何形式化某些东西可能并不清楚，这会导致你在将你的想法转化为形式主义时可能会犯错误 - 你可能 think you proved one thing, when actually you proved another – 或者您可能会发现自己正在进行类型理论研究以形式化一个想法。