给程序员的新逻辑（以及本通讯的未来）New Logic for Programmers (and the future of this newsletter)

所以先说说最近的动态：我刚刚发布了《程序员逻辑》（Logic for Programmers）的 0.14 版本！这个版本和 0.13 相比改动不大。虽然有一些重写，但绝大多数修改都集中在排版、文字润色和技术校对上。完整更新日志请看这里。

顺便提一下，我已经开始为这本书做样书印刷了：

剩下的工作已经不多了。我还需要修复一些图表，进一步调整格式和校对，整合读者反馈的一些修正意见，并制作网站和封底。完成这些之后，这本书应该就可以发布 1.0 正式版本了。我的目标是到六月底之前让大家能买到纸质版！

现在来说个大消息：从八月开始，我将全职加入 Antithesis——一家专注于生成式测试的平台。我的职位是“开发者教育者”，任务是让“基于属性的测试、模糊测试、故障注入、Hegel、Bombadil 以及 Antithesis 平台”变得对普通工程师易于理解。本质上还是我现在在做的工作，只不过会有更多支持，还能享受匹配的 401(k)。

关于这个我已经有了三页的话题想法，你们根本想象不到我有多兴奋

那么这会对通讯产生什么影响呢？首先我要明确一点：它不会变成 Antithesis 的官方通讯。我在 Antithesis 的工作会通过他们的官方渠道发布。但我认为，让某个主题变得“易于理解”的最佳方式之一，就是撰写对全体工程师都有用的基础材料，无论他们是否关注该领域。我可能会分享自己在这方面的创作链接，但也仅限于此。

与此同时，本通讯的内容也会略有调整。属性测试和模糊测试与形式化方法并不相同，但它们有很多共同的基础，尤其是在我们如何思考属性和正确性方面。目前还不确定，但我怀疑我会逐渐将内容偏向与 Antithesis 无关的主题。因此，像“不可判定是什么意思”或“有些测试比其他测试更强”这类偏理论的内容可能会减少，而更多历史背景和软件奇闻异事，比如“为什么叫‘样板代码’”或者冷门编程范式等内容会增加。

另一个变化是频率问题。过去六年我一直保持着（大致）每周更新的节奏。而这六年我也一直是自由职业者。现在有了全职工作，我不知道自己还有多少时间！一旦安顿下来，我还是会继续写通讯，但频率可能会从每周变为双周甚至每月一次。我们会根据实际情况慢慢调整。

总之，这份通讯一直以软件技术为主，最后来点轻松的内容吧。f(x) = x + 2 是一个单调递增函数：x 增大时 f(x) 也增大，x 减小时 f(x) 也随之减小。同样地，f(x) = -x + 1 是单调递减的，而 f(x) = x² 则两者都不是。

在写书的过程中我发现，全称量词在添加元素时是单调为假，在移除元素时是单调为真。设 A(set) = 所有 set 中的 x 满足 P(x)。那么如果 A(S) 为假，A(S | {e}) 也为假；如果 A(S) 为真，A(S - {e}) 也为真。反过来也一样：如果它为真，再添加一个元素仍然为真；如果它为假，去掉一个元素依然为假。

一个有趣的推论是：全称量词对于空集必须为真，因为如果它为假，那对所有集合都应该是假的！这也是 Python 中 all([]) == True 的又一个合理解释。

类似地，在时序逻辑中：始终 A 对系统行为单调地为假，最终 A 单调地为真。我在摆弄朋友（即将成为同事！）Oskar Wickström 的这个 LTL 可视化工具时意识到了这一点。我觉得这挺酷的！