核心问题

程序为什么本质上是逻辑表达？

工程困境

代码不是文字说明，而是机器会执行的命题集合。

if (order.status === "paid") {
  ship(order)
}

这句话在逻辑上说：

如果订单已支付，则允许发货。

Bug 往往不是语法错，而是这个命题在某个场景下不成立。

思想模型

程序 = 条件 + 状态 + 转换 + 不变量。

你写的每个判断，都在定义什么情况下世界可以继续变化。

好判断

写业务逻辑前问：

前置条件是什么？
后置条件是什么？
哪些状态不允许？
哪些条件必须永远为真？

Atlas Action

找一个核心函数，给它补四行注释草稿：

requires:
ensures:
never:
invariant:

不一定提交，但要训练自己先想逻辑。

小结

代码不是步骤堆叠，而是关于系统何时为真的逻辑声明。