review 程序=状态机 gdb 单步执行。 硬件=状态机 程序的本质 程序是一种“数学严格”的对象 打错任何一个字符，编译器都会拒绝。 你写一个程序，实际上是在写 描述 状态机。 程序天生是人类的，连接了人类世界的需求；反人类的一面：程序是在机器上执行的 如何证明一个程序的正确性 1+1 不是公理