依赖类型可以证明您的代码符合规范是正确的。但是你如何证明规范是正确的呢？
Dependent types can prove your code is correct up to a specification. But how do you prove the specification is correct?
依赖类型通常被宣传为一种使您能够断言程序正确符合规范的方法。因此，例如，要求您编写 对列表 进行排序的代码 - 您可以通过将 "sort" 的概念编码为一种类型来证明该代码是正确的，并编写一个函数，例如 List a -> SortedList a。但是如何证明规范 SortedList 是正确的呢？难道不是这样吗，您的规范越复杂，您将该规范编码为类型的可能性就越大？
这是任何规范语言（甚至英语）的问题，而不仅仅是依赖类型。你自己的 post 就是一个很好的例子：它包含 "sort function" 的非正式规范，只需要对结果进行排序，这 而不是 你想要的（\xs -> [] 符合条件）。参见例如this post 来自 Twan van Laarhoven 的博客。
这是 How do you tell that your tests are correct?
的静态类型系统版本
我唯一可以诚实地给出的答案是，是的，您的规范越复杂和笨拙，您犯错的可能性就越大。你可以在类型论形式主义中写一些东西，就像你可以将程序描述形式化为可执行函数一样。
希望您的规范足够简单且足够小，可以通过检查来判断，而您的实现可能要大得多。这有助于，一旦您将一些 "seed" 想法形式化，您就可以证明从这些想法中得出的想法是正确的。从这个角度来看，您越容易从更简单的部分中机械地和可证明地推导出您的规范的某些部分，并最终从您的规范中推导出您的实现，您就越有可能获得正确的实现。
但是可能不清楚如何将某些东西形式化，这会导致您在将想法转化为形式主义时可能会犯错误 – 您可能 think you proved one thing, when actually you proved another – 或者您可能会发现自己在做类型论为了使一个想法形式化而进行的研究。
我认为恰恰相反：类型良好的程序不能证明是无稽之谈（假设系统是一致的），而规范可能不一致或只是愚蠢。所以它不是 "how to make sure this piece of code reflects my platonic ideas?"，而是 "how to make sure my ideas meaningfully project onto a well-founded plane of pure syntactic rules?"。如何确定你看到的鸟是一只反舌鸟 [对于一些提供的反舌鸟概念]？好吧，研究鸟类并增加你正确的机会。但是 always with humans, you can't 100% 确定。
类型理论是一种通过引入正式规则machine-checked proofs（这是一篇非常相关的论文）和其他东西来减轻人类思维不完美的方法，它可以集中注意力，从而大大简化问题（正如 Brouwer 所说："Mathematics is nothing more, nothing less, than the exact part of our thinking")，但你不能指望任何工具来表达你的想法 "right"，因为没有统一的正确概念。 IOW，没有办法正式连接非正式和正式：非正式就像在 IO monad 中——没有逃脱。
所以它不是 "does this syntax reflects my very precise semantics?"，而是 "can I attach my raw semantics to this strongly structured syntax?"。程序是适当的 material 对象，而想法是繁琐的近似值，只有按照约定才能成为适当的 material 对象。因此，我们使用约定形成一些基础，然后我们就相信它，因为相信你众多想法中的一小部分比相信所有想法要明智得多。
你如何证明数学是正确的？即，如何证明整数加法是数苹果的正确方法，或者如何证明实数加法是正确的权重相加方法？正式/数学和非正式/真实之间总是有一个接口。它需要技巧和数学/物理品味来找到解决特定问题的合适形式。正式方法不会消除这一点。
形式化方法的价值是双重的：
您不会知道您的程序是否正确，除非您知道它实际满足哪些属性。在您知道您的排序例程是否为 "correct" 之前，您首先必须知道它实际上做了什么。任何发现这一点的程序都将是一种正式的方法（甚至是单元测试！），所以拒绝 "formal methods" 的人实际上只是将自己限制在可用方法的一小部分。
即使您知道如何找出程序的实际作用，人们也会在数学推理中犯错误（我们不是理性动物，无论确定意识形态可能声称）；所以让机器检查我们很有帮助。这与我们使用单元测试的原因相同——运行 桌面检查并确保程序执行我们想要的是很好的；但是让计算机进行检查并告诉我们结果是否正确有助于防止错误。出于完全相同的原因，让计算机检查我们关于程序行为的证明是有帮助的。
形式化方法可以做的一件事是帮助将简单的事物与更复杂的事物联系起来，但我认为其他人没有触及。您可能不确定如何准确指定 Set 数据结构的行为方式，但是如果您可以编写一个基于排序列表的简单版本，那么您就可以证明您的基于平衡搜索树的奇特版本与它通过 toList 功能正确。也就是说，您可以使用形式化方法将您对排序列表的信心转移到平衡搜索树。
假设你的函数不是顶级函数，而是被其他人用作某个模块的一部分，该模块也有正确性证明。后者必须使用你的功能的正确性证明，如果它是坏的，模块将不会编译。模块本身还是会出错，但已经不是你的问题了
聚会迟到了，但是 AFAICT，还没有人提到另一个重要方面：在程序验证的上下文中，规范中有错误并不总是太可怕，因为您可以使用 code 检查 spec.
IOW，证明不是"the code is right"，而是"the code and the spec are mutually consistent"。因此，为了使规范中的错误不被注意，它必须是以下之一：
- 未指定规格。
- 规范中的错误与代码中的相应错误相匹配。
正如其他人所指出的：测试的问题是一样的。
依赖类型通常被宣传为一种使您能够断言程序正确符合规范的方法。因此，例如，要求您编写 对列表 进行排序的代码 - 您可以通过将 "sort" 的概念编码为一种类型来证明该代码是正确的，并编写一个函数，例如 List a -> SortedList a。但是如何证明规范 SortedList 是正确的呢？难道不是这样吗，您的规范越复杂，您将该规范编码为类型的可能性就越大？
这是任何规范语言（甚至英语）的问题，而不仅仅是依赖类型。你自己的 post 就是一个很好的例子：它包含 "sort function" 的非正式规范，只需要对结果进行排序，这 而不是 你想要的（\xs -> [] 符合条件）。参见例如this post 来自 Twan van Laarhoven 的博客。
这是 How do you tell that your tests are correct?
的静态类型系统版本我唯一可以诚实地给出的答案是，是的，您的规范越复杂和笨拙，您犯错的可能性就越大。你可以在类型论形式主义中写一些东西，就像你可以将程序描述形式化为可执行函数一样。
希望您的规范足够简单且足够小，可以通过检查来判断，而您的实现可能要大得多。这有助于，一旦您将一些 "seed" 想法形式化，您就可以证明从这些想法中得出的想法是正确的。从这个角度来看，您越容易从更简单的部分中机械地和可证明地推导出您的规范的某些部分，并最终从您的规范中推导出您的实现，您就越有可能获得正确的实现。
但是可能不清楚如何将某些东西形式化，这会导致您在将想法转化为形式主义时可能会犯错误 – 您可能 think you proved one thing, when actually you proved another – 或者您可能会发现自己在做类型论为了使一个想法形式化而进行的研究。
我认为恰恰相反：类型良好的程序不能证明是无稽之谈（假设系统是一致的），而规范可能不一致或只是愚蠢。所以它不是 "how to make sure this piece of code reflects my platonic ideas?"，而是 "how to make sure my ideas meaningfully project onto a well-founded plane of pure syntactic rules?"。如何确定你看到的鸟是一只反舌鸟 [对于一些提供的反舌鸟概念]？好吧，研究鸟类并增加你正确的机会。但是 always with humans, you can't 100% 确定。
类型理论是一种通过引入正式规则machine-checked proofs（这是一篇非常相关的论文）和其他东西来减轻人类思维不完美的方法，它可以集中注意力，从而大大简化问题（正如 Brouwer 所说："Mathematics is nothing more, nothing less, than the exact part of our thinking")，但你不能指望任何工具来表达你的想法 "right"，因为没有统一的正确概念。 IOW，没有办法正式连接非正式和正式：非正式就像在 IO monad 中——没有逃脱。
所以它不是 "does this syntax reflects my very precise semantics?"，而是 "can I attach my raw semantics to this strongly structured syntax?"。程序是适当的 material 对象，而想法是繁琐的近似值，只有按照约定才能成为适当的 material 对象。因此，我们使用约定形成一些基础，然后我们就相信它，因为相信你众多想法中的一小部分比相信所有想法要明智得多。
你如何证明数学是正确的？即，如何证明整数加法是数苹果的正确方法，或者如何证明实数加法是正确的权重相加方法？正式/数学和非正式/真实之间总是有一个接口。它需要技巧和数学/物理品味来找到解决特定问题的合适形式。正式方法不会消除这一点。
形式化方法的价值是双重的：
您不会知道您的程序是否正确，除非您知道它实际满足哪些属性。在您知道您的排序例程是否为 "correct" 之前，您首先必须知道它实际上做了什么。任何发现这一点的程序都将是一种正式的方法（甚至是单元测试！），所以拒绝 "formal methods" 的人实际上只是将自己限制在可用方法的一小部分。
即使您知道如何找出程序的实际作用，人们也会在数学推理中犯错误（我们不是理性动物，无论确定意识形态可能声称）；所以让机器检查我们很有帮助。这与我们使用单元测试的原因相同——运行 桌面检查并确保程序执行我们想要的是很好的；但是让计算机进行检查并告诉我们结果是否正确有助于防止错误。出于完全相同的原因，让计算机检查我们关于程序行为的证明是有帮助的。
形式化方法可以做的一件事是帮助将简单的事物与更复杂的事物联系起来，但我认为其他人没有触及。您可能不确定如何准确指定 Set 数据结构的行为方式，但是如果您可以编写一个基于排序列表的简单版本，那么您就可以证明您的基于平衡搜索树的奇特版本与它通过 toList 功能正确。也就是说，您可以使用形式化方法将您对排序列表的信心转移到平衡搜索树。
假设你的函数不是顶级函数，而是被其他人用作某个模块的一部分，该模块也有正确性证明。后者必须使用你的功能的正确性证明，如果它是坏的，模块将不会编译。模块本身还是会出错，但已经不是你的问题了
聚会迟到了，但是 AFAICT，还没有人提到另一个重要方面：在程序验证的上下文中，规范中有错误并不总是太可怕，因为您可以使用 code 检查 spec.
IOW，证明不是"the code is right"，而是"the code and the spec are mutually consistent"。因此，为了使规范中的错误不被注意，它必须是以下之一：
- 未指定规格。
- 规范中的错误与代码中的相应错误相匹配。
正如其他人所指出的：测试的问题是一样的。