第三法

Belleve Invis

· 2017-03-22

我们离写出正确的程序还有多远？

这里的「正确」不仅仅是通过测试那么简单，而是要保证逻辑学层面的「正确性」，即至少可以满足逻辑命题的程度。比如考虑下面的翻转二叉树：

data Tree : Type -> Type where
	Leaf : a -> Tree a
	Branch : a -> Tree a -> Tree a -> Tree a

flipTree : Tree a -> Tree a
flipTree (Leaf x) = Leaf x
flipTree (Branch x l r) = Branch x (flipTree r) (flipTree l)

「逻辑命题程度的正确性」有两种保证的方法，一种是使用逻辑证明，即基于 Curry-Howard 同构的手段，在程序语言中用类型表示命题，然后用定义属于此类型的函数的方法证明之，如

flipTreeSym : (t : Tree a) -> t = flipTree (flipTree t)
flipTreeSym (Leaf x) = Refl
flipTreeSym (Branch x l r) = do
	let recL = flipTreeSym l
	let recR = flipTreeSym r
	rewrite recL in 
		rewrite recR in Refl

这属于最强力的手段，如此写出的证明效力等同数学定理，但缺点也很明显，撰写证明十分困难。有些编程语言或者「证明助手」提供了 Tactic 的手段，但仍然没有大幅度降低证明的难度。稍弱些的手段则是如 Haskell 的 Quickcheck 一般，使用普通的布尔表达式描述程序应该满足的要求，并使用自动化生成的测试案例去测试。

换言之，目前的技术手段已经可以让我们确保我们所写程序是正确的。我们的处境是，我们已经站在了一个通向「写正确的程序」的路口，这条路看上去十分曲折，但里程碑已经显现，我们应该起身探索了。

前几天和 @雾雨魔理沙讨论未来的编程语言的时候，我们的想法是，它很可能是某个支持 Dependent Type，支持 Programming / Proof by Refinement 的语言，配合做 Term Unification / ATP 的插件降低难度。

——这三点就是标题里面的「第三法」，保证正确性的解决方案，或者说就是所谓的「The Last 700 Programming Languages」。

Dependent Type：允许程序员以简单直接的方式约定他想要写的程序应该满足的性质，并且可以用形式证明，或 QuickCheck 类测试，或传统测试确保。三者的成本逐渐下降，正确性也逐渐下降，但是三者结合，便平衡正确性与成本。除证明测试外，Dependent Type 带来的强大类型描述能力也可以将入口细化，降低程序员出错的概率。

Programming / Proof by Refinement：允许程序员以逐步细化的方式实现非常复杂的约束。比如魔理沙那个 DeepDarkFantasy 里面有这样一个类型非常吓人的函数：

hlam :: forall repr a b h. DBI repr =>
	((forall k. NT (repr (a, h)) k => k a) -> (repr (a, h)) b) ->
	repr h (a -> b)

但如果使用类似于 Coq 的 LTac，写出来并不算非常困难：

{`hlam` = tactic {}	{(`repr`, `a`, `b`, `h`) ← intros `4`}
{}	{`i`{`DBI`, `repr`} ← intro}
{}	{`f` ← intro}
{}	{apply `i`{`DBI`, `repr`}.hoas}
{}	{`x` ← intro}
{}	{apply `f`}
{}	{`k` ← intro}
{}	{`i`{`NT`, `reprah`, `k`} ← intro}
{}	{apply `i`{`NT`, `reprah`, `k`}.conv}
{}	{exactly `x` }}

在搭建的过程中通过一点点拆解复杂的目标，最终写出整个程序出来。上面的「Tactic」看着玄乎，实际上只是搭积木一样的过程而已。

Programming/Proof by Refinement 的过程实际上还可以和 Property-based testing 结合，比如如果某一步中出现的 goal 或者 assert 测试不过，那么就可以直接在交互界面显示出来，等等。

Term Unification / ATP：如果 Programming/Proof by Refinement 还是觉得麻烦怎么办？别忘了上面的 Tactic 是一块块的积木，那么能不能写插件去自动地把积木拼上呢？如果结合现在发展迅猛的人工智能呢？这已经不是遥不可及的事情了。

总上而言，我们离「写正确的程序」已经越来越近。

如果说编程有未来的话，这个才是值得期待的未来。

「第三法」之下的美丽的未来。