《Logic for Programmers》新版本（以及本通讯的未来）

<p>首先，有一条即时消息：我刚刚发布了 <a href="https://logicforprogrammers.com" target="_blank">《Logic for Programmers》</a> 的 0.14 版本！这个版本与 0.13 版本非常相似。虽然有一些重写，但绝大多数改动都是布局、文字编辑和技术编辑。完整说明见<a href="https://github.com/logicforprogrammers/book-assets/blob/master/CHANGELOG.md" target="_blank">此处</a>。</p> <p>相关消息是，我已经开始打印该书的测试版本：</p> <p><img alt="《Logic for Programmers》的两个测试打印版" class="newsletter-image" src="https://assets.buttondown.email/images/958bdc79-fa06-4bce-b0a8-6e5ecfe8f2e0.png?w=960&amp;fit=max" /></p> <p>剩下的工作不多了。我还需要修复一些图表，进行更多排版和校对，整合读者提出的修正，并制作网站和封底。之后，这本书应该就能达到 1.0 版本。我的目标是到 6 月底就能买到印刷版！</p> <hr /> <p class="empty-line" style="height:16px; margin:0px !important;"></p> <p>现在说重大消息：从八月开始，我将全职加入 <a href="https://antithesis.com/" target="_blank">Antithesis</a>，这是一个生成式测试平台。我的正式职位是“开发者教育者”，我的任务是让“基于属性的测试、模糊测试、故障注入、<a href="https://hegel.dev/" target="_blank">Hegel</a>、<a href="https://github.com/antithesishq/bombadil" target="_blank">Bombadil</a> 以及 Antithesis 平台变得对日常工程师易于理解”。所以这和我现在做的工作类似，只是得到了更多支持，还有相匹配的 401(k) 计划。</p> <p>我已经有三页纸的主题想法了，你想象不到我有多兴奋。</p> <p>那么这对本通讯有什么影响呢？首先，我想明确一点：这不会变成一份 Antithesis 通讯。我与 Antithesis 相关的工作将放在他们的官方平台上。我确实认为，让一个主题“易于理解”的最佳方式之一，就是撰写对所有工程师都有用的基础材料，无论他们是否深入该主题。我可能会分享一些我在这方面所做内容的链接，但这些仅仅是链接而已。</p> <p>与此同时，本通讯的内容也会有些变化。基于属性的测试和模糊测试与形式化方法并不相同，但许多基础是重叠的，尤其是在我们思考属性和正确性方面。我还不确定，但我感觉我会开始让本通讯远离 Antithesis 相关主题。所以可能会减少理论性内容，比如<a href="https://buttondown.com/hillelwayne/archive/what-does-undecidable-mean-anyway/" target="_blank">“不可判定究竟意味着什么”</a>和<a href="https://buttondown.com/hillelwayne/archive/some-tests-are-stronger-than-others/" target="_blank">“有些测试比其他测试更强”</a>，增加更多历史和软件奇闻轶事，比如<a href="https://buttondown.com/hillelwayne/archive/why-do-we-call-it-boilerplate-code/" target="_blank">“我们为什么称之为‘样板代码’”</a>和<a href="https://buttondown.com/hillelwayne/archive/finding-hard-24-puzzles-with-planner-programming/" target="_blank">“深奥的编程范式”</a>。</p> <p>另一个变化是更新频率。过去六年里，我基本保持每周更新。同时，过去六年我也是完全自雇状态。我不知道有了全职工作后会有多少时间！一旦稳定下来，我希望继续写通讯，但可能从每周降到双周或每月。我们边走边看吧。</p> <hr /> <p>总之，这期通讯软件相关的内容较少，所以让我们用一个有趣的东西来收尾。<code>f(x) = x+2</code> 是 <strong>单调递增函数</strong>：增大 <code>x</code> 会使 <code>f(x)</code> 增大，减小 <code>f(x)</code> 会使 <code>x</code> 减小。类似地，<code>f(x) = -x+1</code> 是单调递减函数，而 <code>f(x) = x^2</code> 则两者都不是。</p> <p>在写书的过程中，我意识到全称量词在添加元素时是单调假，在移除元素时是单调真。设 <code>A(set) = all x in set: P(x)</code>。那么如果 <code>A(S)</code> 为假，则 <code>A(S | {e})</code> 也为假；如果 <code>A(S)</code> 为真，则 <code>A(S - {e})</code> 也为真。<code>some</code> 则相反：如果它为真，添加元素后仍为真；如果它为假，移除元素后仍为假。</p> <p>一个有趣的推论是，全称量词对空集必须为真，因为如果它为假，则对所有值都为假！这也是 Python 中 <a href="https://buttondown.com/hillelwayne/archive/why-all-is-true-prod-is-1-etc/" target="_blank"><code>all([]) == True</code></a> 的另一个理由。</p> <p>类似地，在时序逻辑中：<code>always A</code> 在系统行为上是单调假，而 <code>eventually A</code> 是单调真。我是在摆弄我的朋友（很快就是同事了！）Oskar Wickström 制作的这个 <a href="https://quickstrom.github.io/ltl-visualizer/" target="_blank">LTL 可视化工具</a> 时意识到这一点的。我觉得这很酷！</p> <p class="empty-line" style="height:16px; margin:0px !important;"></p>