buttondown-com-hillelwayne

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

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文档记录问题分析、解决方案讨论和思维过程，帮助经验相对不足的合作伙伴理解复杂概念变更，避免因理解不充分导致代码或规范难以维护。

作者在完成《程序员逻辑》一书后，首次在五个月内更新博客，分享了一些有趣的Z3脚本示例。文章讨论了书中未采用的"废料"内容，并解释了选择特定数学属性进行证明的考量过程。

本周因事务繁忙暂停通讯，作为补偿提供十本《程序员逻辑学》免费副本。其中五本现已可领取，另外五本因Leanpub平台技术问题暂时无法提供。

作者通过分析AI生成的TLA+和Alloy规范案例，指出大型语言模型在编写形式化规范时存在严重问题：它们倾向于生成"显而易见"但无实际验证价值的属性，而无法捕捉并发、非确定性或多步骤交互中的微妙错误。即使AI降低了形式化方法的入门门槛，但若用户本身缺乏专业知识，仍难以获得真正有用的验证结果。

文章主张在技术选择上应保守，采用成熟稳定的"乏味技术"，而在开发实践上可以大胆创新。因为技术变更成本高昂且维护负担重，而实践方法可以灵活调整和放弃，不会留下长期的技术债务。

作者在四月愚人节特辑中探讨了纽约与芝加哥披萨之争，认为这种争论本身是错位的，并借此机会深入介绍了芝加哥的美食文化，特别是其独特的深盘披萨与香肠特色。

本文探讨了规范与代码的区别：规范对应一组可能的实现，而代码只是其中的单一实现。即使规范足够全面和精确，它仍然是一种抽象，而非代码本身。作者强调保持"规范"和"代码"作为不同概念的重要性。