buttondown-com-hillelwayne

作者讨论了"所有程序员都能从学习数学中受益"与"所有程序员都需要学习数学"之间的区别。他认为，广泛了解多个领域的皮毛比深入学习某一个具体领域更有用——因为只有先知道某个领域存在且可能有帮助，才会决定是否深入钻研。文章建议通过阅读本科教材或会议视频等方式获取广泛的学科概览。下周因参加布达佩斯Craft大会，将暂停一次常规通讯。

本文通过逻辑推理阐述了"添加假设会使系统属性变弱"的核心观点。作者用形式化方法说明，一个无假设的属性（如"系统能正确解析有效JSON"）比带假设的属性（如"仅当输入为ASCII时系统能正确解析有效JSON"）更强，因为后者只在假设成立时才保证正确性。文章还探讨了我们为何需要引入假设的三个原因：属性本身无法满足、成本过高、或难以验证。最后指出，检验假设是否成立通常是一个独立且更复杂的问题。

本文揭示了排版领域一个令人惊讶的事实：LaTeX 和 Inkscape 虽然都使用"点"（pt）作为度量单位，但两者定义不同。LaTeX 采用传统印刷点（1/72.27 英寸），而 Inkscape 继承自 PostScript 的计算机点（1/72 英寸），两者相差约 0.4%。文章追溯了点作为排版单位的混乱历史——从 16 世纪诞生至今，不同国家、不同技术体系对"点"的定义始终未能统一，从 NIST 的官方定义到 Donald Knuth 在 TeX 中的微调，再到 W3C 标准的选择，这段历史充满了测量精度、标准化妥协与技术传承的有趣故事。

作者发布了《程序员逻辑》一书 0.14 版本，主要涉及排版、文案和技术编辑的改进，并计划在六月底前推出印刷版。更大的消息是，从八月起作者将全职加入 Antithesis 公司担任开发者教育者，负责让属性测试、模糊测试、故障注入等概念对普通工程师变得可理解。这也意味着本通讯的内容将有所调整，可能会减少形式化方法等理论话题，增加历史与软件趣事类内容；同时更新频率可能从每周一次降至每两周或每月一次。

非法状态（illegal state）是系统绝不应进入的状态，而非期望状态（unwanted state）则是我们不愿停留的状态。许多我们以为是非法状态的情形，实际上只是非期望状态。例如日程冲突在系统中可以临时存在（用户可能需后续处理），但飞机超售必须在登机前解决，否则将演变为非法状态。系统需要具备检测和处理非期望状态的能力，有时甚至需要主动允许这些状态存在，以支持特定业务流程（如航空公司超额预订）。从形式化角度看，非法状态对应违反的不变量（[]!Illegal），而非期望状态可用热状态（hot states）或更强属性来描述。

本文探讨了TLA+语义保证与模型检查器实现之间的差异，解释了为什么初学者在使用PrintT等副作用操作符时会遇到困惑，以及这种抽象泄漏如何影响编程体验。

本文介绍了逻辑量词（全称量词和存在量词）在软件开发中的应用，包括如何用它们表达软件属性、简化代码模式，以及通过量词对偶性处理数据库约束等实际用例。

Hillel Wayne 的自出版书籍《程序员逻辑学》迎来发布一周年。该书目前版本为 v0.10，已售出 1180 册，作者计划在夏季完成重大重写，秋季进行编辑和设计，冬季发布 1.0 正式版。这本书填补了软件教育材料的空白，作者对最终版本充满期待。

作者通过自身从VSCode切换回Neovim后生产力显著提升的经历，质疑了"编码不是软件开发瓶颈"的普遍观点。他认为即使写作速度提升100倍，即使阅读和理解能力不变，也能通过快速编写工具、尝试更多实验性编辑等方式大幅提升开发效率。

本文探讨了编程语言中的"逃生舱口"概念——这些特性允许开发者突破语言的核心假设以增加功能。从Rust的unsafe代码到C++的内联汇编，作者分析了这些功能如何平衡语言能力与可预测性，并讨论了使用逃生舱口可能带来的问题。

本文探讨了数组的概念模型，将一维数组视为定义在整数区间上的函数，并扩展到多维数组和表格。作者通过函数式编程的视角解释了APL风格的多维数组与表格之间的本质区别，特别是异构数据结构如何限制了表格的多轴扩展能力。

作者分享了他希望存在但尚未找到的软件工程书籍清单，包括配置管理、复杂数据模式、计算机科学基础、MISU设计模式、现代工具指南、历史优化技术以及Sphinx内部机制等主题。这些书籍将帮助开发者更深入地理解软件工程的核心概念和实践。

文章探讨了萨丕尔-沃尔夫假说在编程语言领域的适用性，认为编程语言对思维方式的影响更像是"俄罗斯方块效应"——即通过大量练习获得的技能会改变认知模式，而非语言本身决定思维结构。作者通过不同编程范式解决同一问题的示例说明，虽然编程语言会影响问题解决方式，但这更多是技能习得的结果，而非语言决定论的体现。

本文探讨了逻辑对偶在软件工程中的应用，重点介绍了量词对偶（存在与全称量词的相互转换）如何使各种软件工具既能查找满足条件的值，又能验证所有值都满足属性。文章通过Z3、属性测试、模型检查器等实例展示了这种对偶关系在实际工程中的强大应用。

本文探讨了形式化方法中的两种非确定性：恶魔式非确定性假设系统总是做出最坏选择，用于验证所有路径都满足属性；天使式非确定性假设系统总是做出最佳选择，用于验证存在满足属性的路径。后者在复杂性分析和编程语言中更为常见，如NP问题的定义就基于天使式非确定性。

作者指出许多看似困难的算法面试问题，如找零钱问题、股票买卖问题等，实际上可以通过约束求解器轻松解决。使用MiniZinc等工具，只需几行代码就能表达问题约束，而无需编写复杂的动态规划算法。

作者原计划在本周简报中简要介绍代数数据类型的历史，但最终写成了一篇长达3500字的详细博客文章。文章追溯了代数数据类型的早期发展历程，并附有Patreon博客笔记链接。

本文探讨了即使经过形式化验证的代码仍可能出现错误的三种情况：证明本身无效、规范属性错误、以及基本假设错误。作者通过"左填充"函数验证失败的案例，揭示了形式化验证中"正确性"概念的模糊边界。

作者通过自己从5公里到10公里的跑步突破，探讨了技能学习中的"相变"现象——进步不是线性的，而是在某个临界点突然发生质变。文章提出了两个问题：能否加速相变的发生，以及如何激励人们坚持到相变发生。

文章探讨了模态编辑（如Vim中的模式切换）并非因其内在优势而流行，而是源于历史偶然。作者认为，如果没有Bill Joy在50年前创建vi，今天可能根本不会有模态编辑器存在。模态编辑最初是Xerox的一个实验性功能，后来因vi随BSD Unix免费分发而普及，但其本身并未在其他软件领域广泛传播。

作者因撰写每周软件文章感到倦怠，从最初只需一个下午到现在需要两三天时间，加上工作和生活上的短期优先事项，决定暂停《Computer Things》专栏至年底，2026年前不再尝试每周更新节奏。

即日起至月底，使用优惠码"feedchicago"可半价购买《程序员逻辑学》电子书，所有版税将捐赠给大芝加哥食品储藏室，支持当地食品银行。

作者为芝加哥大区食品库发起的《程序员逻辑》电子书五折慈善募捐活动还剩最后一周，目前已筹集超过1600美元。同时作者分享了关于编程语言中"野生goto"与"驯服goto"的有趣历史探讨。

这篇文章分享了多个有趣的软件冷知识，包括在康威生命游戏中实现俄罗斯方块、Vim的图灵完备性、反斜杠字符的起源、银河算法、Cloudflare用熔岩灯生成随机数等。这些事实展示了软件世界中的奇妙现象和历史趣闻。

本文探讨了里氏替换原则不仅适用于继承关系，其关于前置条件和后置条件的规则可应用于任何代码替换场景，包括API版本更新。通过形式化分析展示了新版本代码必须满足比旧版本更弱的前置条件和更强的后置条件才能保证兼容性，这为软件维护和演化提供了重要指导。

作者在编写《程序员逻辑》新版时重新体验了Prolog的痛点，包括缺乏标准化字符串、没有函数、集合类型有限、无布尔值、cut操作符令人困惑等问题。虽然Plog的双向性很强大，但这些设计缺陷让作者更倾向于使用Picat语言。

本文通过数据库迁移案例探讨了精化概念：如何在保持外部属性不变的前提下，将布尔字段转换为时间戳字段，再进一步转换为事件溯源模型。文章展示了通过定义精化映射函数，新系统可以兼容旧代码，同时讨论了可变性约束对精化的影响。

《程序员逻辑学》v0.13版本正式发布，全书已超过5万字，所有章节都经过重写。作者将重点转向领域建模教学，并加强了章节间的联系。目前书稿已交付编辑，进入出版准备阶段。

本文探讨了形式化方法中的可能性属性P(x)，它表示"x在模型中可能发生"，这是安全性和活性属性之外的重要第三类属性。作者讨论了如何用可能性属性验证规范的正确性，并指出虽然主流工具如Alloy和TLA+不原生支持P(x)，但简单的可达性属性可以通过A(!x)的反例来验证。

作者在结对编程时尝试了一种新方法：通过创建Markdown文档记录问题分析、解决方案讨论和思维过程，帮助经验相对不足的合作伙伴理解复杂概念变更，避免因理解不充分导致代码或规范难以维护。