拿硬件打个比方说明什么是计算机科学
发布时间： 2024-12-10 12:59:47
比如一个运算放大器，opamp，它有一个 model，它的 input 会转换成 output，它可以搭配一个无源器件网络实现信号的变换，包括不同频率的不同放大倍数。
这里的每个器件都被物理学定律 govern，这相当于他们的 operational semantics，就像我们在计算机语言里定义的那样。
计算机语言当然也是有 model 的，但是一段程序的 operational semantics 很变态，尤其是传入参数可能带着一根指向宇宙的指针，这就吐血了。
一颗运算放大器的内部并不简单，但是它有一个 ideal model 的描述，当一个放大器经过简单组合成为 4-stage 8th order low pass filter 时，我们发现它的 semantics 的 composition 产生的结果，仍然是足够简单的，这一点是计算机语言表达的程序非常难以做到的。
在很大意义上说计算机语言被称为语言是一个谎言，因为如果一大坨语言描述都是语法上的，它没有解决用户需要用语言表达「meaning」的需求，或者「meaning」没办法简单被理解，这个就失去了语言的意义。
所以今天的计算机语言，说它是 formal language，这是对的，但如果说程序是 formal system，definitely no，因为 compiler 最终只是把它拿去翻译成机器指令让计算机可以运行这段程序，这就是「中国盒子」的例子；虽然今天的计算机语言实现，类型系统的设计，编译优化等等，无论在工程上还是在科学上都比龙书出来的时候大有进步，但是，龙书封面上写的那句：
syntax directed translation
依旧是现代计算机语言的本质。
++++
而 fix 这个问题的办法其实就是定理证明器，无论是 proof assistant 还是 automatic theorem prover。
它和计算机语言的本质区别是，数学上一定要定义 equality，一定要能够用 predicate 表达 property，这两点都是现代计算机语言缺乏的，而定理证明器具备的。equality+definition (Russell's definite description theory) 在非常大的意义上意味着 formalize meaning。
实际上没有什么困难阻止计算机语言和定理证明器二合一，Racket 语言可以写一个程序把 Racket 代码拿进来证明一段 code 是具有某个 property 的，这是完全可以做到的。类似的，现代定理证明器搜索证明的技术，term finding，实际上就是在写代码，或者说找出一段代码可以满足表达 property 的 predicate。
Furthermore，简单的代码例如排序，已经有基于 smt solver 和一个 combinator pool 的暴力搜索可以写出，这或多或少给算法老师的入门课的前途蒙上一层阴影。
++++
回到前面的硬件隐喻我们会发现，电子电路的 simulation 软件就是一定意义上的 proof assistant，它知道所有器件的 operational semantics（spice model），它有一个求解器，不是万能但是能解决很多问题，因为求解器和电路设计者有一些 common sense 和 best practice 的 knowledge 在，虽然这是 domain specific 的，但是很重要它是可以被表达的，例如用户可以输入一个 5V 电源，产生 PWM 波形，能设定上升沿下降沿以及占空比。
在计算机语言里，你可以在 function 名字和参数名字上体现这些，但仅仅是名字而已，编译器或者开发环境都不能 get 到他们的 meaning，它对程序的语义堪称一无所知，也不会让你表达什么 property 或 constraint 帮你 check，除了类型能表达很有限的那点东西。
++++
总结：
计算机语言的未来将是融合定理证明器，能表达语义，能表达定义，能用逻辑表达式表达 specification，局部的，能自动搜索代码，就算搜索不到代码也可以留下 hole 先当它是公理完成程序构建，留下的 hole 可以等待数学能力更好的人来给出证明。
这样的程序才是 fully formalized，这个工程方法，才能被称为计算机科学，否则跟手工业盖房子没区别。计算机和计算机语言只是高级铁锹而已。
