Turing和Post这代人就是这么编程的,相比之下什么brainfucking语言并无新意,也没有更难.

Turing machine的问题在于它是100% local的;这个问题在今天的编程语言里仍然存在,只是因为函数形式的引入,有一定改善.但是对于有规模的程序来说,仍然困难.

如果用proof和program对比,proof的bottom up结构更清晰一点,对应program,则是函数和参数构成的tree结构,lambda和组合子都有这种tree结构;这大概也是Alan Perlis在计算机语言理论与实践中引入lambda的最初原因,用top down的方式组织程序.

当然这个在sequential program时代非常成功的做法,随着程序规模更大和并发与网络计算的引入,受到了新的挑战,到目前为止还没有一统江湖的canonical model出现.