程序与文档

通过半年的实践，期间也断断续续的在折腾本身所写的一个文式编程工具。如今能够正式但不严肃的谈谈对文式编程的一些体会了。

写程序不难，关键是写出有用的程序。

写出有用的程序也不难，关键是写出可以让别人继续维护下去的程序。

文档是重要的，没有文档，单凭代码中那些常常很蹩脚的变量名与函数名，每每很难理解一段代码的功能及用途。$y=ax^2$ 是抛物线吧？那 $E=mc^2$ 是什么？编程虽然也像数学那样依赖于符号，但它更像是物理学。

编程语言所提供的注释机制能够解释代码，可是它不能替代程序文档。若是将一个程序视为一部电影，那么代码的注释像是电影里的旁白，而程序的文档则是这部电影的剧本。

阅读没有文档的程序源码，阅读者弄懂这些源码的过程，本质上只是为这些源码从新撰写了一份文档。去为一份并不是本身编写的程序源码重建文档，困难系数一般远大于程序源码的做者本人来写。

写文档，所耗费的精力与时间每每要大于写编写程序源码的时间。这是不少程序缺少文档——抑或有文档，可是文档每每落后于源码几个世纪的缘由之一。另一个缘由，写程序的人多为理工科出身，文字表达能力一般比较着急。虽然 Knuth 于上个世纪 70 年代就在倡导文学编程的理念，可是迄今为止还没据说过哪一个写程序的人用文学编程写出了一部发人深省的做品。不过，可能更主要的缘由是，老板们不会为此多给钱，甚至会由于你代码写的慢而开掉你。

这一现实让我很差意思在这里谈什么文学编程，仍是弱化一下，称之为『文式编程』更好一些。

按照柯里-霍华德同构定理，写程序的过程与证实一个数学命题的过程是等价的。也就是说，咱们写程序，本质上就是一连串的推理过程，当程序可以运行起来，而且可以正确的解决咱们要解决的问题之时，这意味着咱们已经完成了一个数学命题的证实。若是将这个推理的过程用文档记述下来，而且将程序的源码也嵌入这个推理的过程之中，做为每一个推理阶段的所得结果，这样就实现了程序文档与源码的融合。这样的结果一定不是文学做品，而是一篇论文。

每一个人写程序的过程，实际上是有程序文档的，只不过他们没有把它写出来。他们像拍电影同样，基于剧本，一个镜头一个镜头的将电影拍出来，而后烧掉了剧本。

要用好文式编程，必需要按照一个问题的推理顺序将文档与代码一并写出来。