The hope is that your specification is simple and small enough to judge by examination,while your implementation of that might be far larger.
这种推理对我来说很有意义. Idris是测试这些概念最容易理解的语言;然而,由于它几乎可以像Haskell一样使用,它常常让程序员在旧概念中游荡,而不知道在哪里应用依赖类型.一些现实世界的例子可以对此有所帮助,那么,在实践中发生的程序的具体例子是什么,很容易表达为类型,但实现起来很复杂？
假设我们有f :: Ord a => [a] – > [a](我将使用Haskell表示法).我们对这个函数f了解多少？换句话说,你可以预测f [],f [5,8,7],f [1,1,2,2]等应用程序？假设您知道f x = [4,6,8]那么您对x有什么看法？你可以观察到,我们知之甚少.
然后假设我告诉你f的真实名字是排序.那么关于那些相同的例子你能告诉我什么？你能告诉我关于fss = ys中xs的ys是什么意思？现在你知道了很多,但这些信息来自哪里？我所做的只是改变功能的名称;这对程序的正式含义没有意义.
所有这些新信息都来自您对排序的了解.你知道两个定义特征：
> sort xs是xs的排列.
> sort xs是单调递增的.
我们可以使用依赖类型来证明这两个属性的排序.然后,这不仅仅是我们对分类的外在理解的问题;排序的意义成为程序的内在组成部分.
捕获bug是副作用.真正的目标是作为计划的一部分,在我们的头脑中指定和形式化我们必须知道的内容.
仔细重新考虑您已编写的程序.什么使你的程序工作的事实只在你的头脑中知道？这些都是候选人的例子.
