第三法

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

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

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)intros4}
{} {i{DBI,repr}intro}
{} {fintro}
{} {applyi{DBI,repr}.hoas}
{} {xintro}
{} {applyf}
{} {kintro}
{} {i{NT,reprah,k}intro}
{} {applyi{NT,reprah,k}.conv}
{} {exactlyx}}

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

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

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

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

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

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