为什么人们不使用形式化方法？
作者梳理了形式化方法在工程界长期未被普及的历史脉络与核心障碍，指出证明过程的高门槛、规格定义的困难以及性价比问题才是主因。
评论
点赞
收藏程序员的逻辑现已可用
我很高兴地宣布，我的书，程序员逻辑， 现已上市！你可以去看看发布网站在这里 或者直接去买电子书 或印刷版本.如果你买了抢先体验版本，可以免费从leanpub. 这酝酿已久。形式逻辑是一个极其强大的工具来理解软件。从“什么是左外接合”到“为什么不应该这样”，各种问题都有Square继承自Rect如果你懂一些基础逻辑，这才更合理。然而实际上并没有任何专门针对程序员的资源学习那些基础知识。你只是被期望打...
芝加哥与纽约披萨之争是个伪命题
作者认为芝加哥深盘披萨与纽约薄底披萨属于不同消费场景，不应直接比较。作者提出真正的对标物是纽约披萨与芝加哥热狗，并从便携性、家庭制作难度等角度进行对比，最后延伸至意大利牛肉三明治等其他芝加哥美食。文章以个人经验和幽默视角解构经典美食争论。
我们是工程师吗？关于软件身份认同的深度调查
作者通过采访17位从传统工程跨界到软件开发的从业者，探讨软件工程师身份认同问题。文章反驳了软件缺乏数学基础、后果不严重或无需执照就不是工程的观点，指出传统工程界内部定义也模糊，多数跨界者认可软件工程的工程属性，并区分了软件开发与软件工程的差异。
一些有趣的 Z3 脚本评论汇总
作者 Hillel Wayne 汇总了此前发布的 Z3 脚本文章收到的读者反馈、相关博客链接及邮件评论，属于社区互动内容的整理。
我写的一些Z3求解器趣味脚本
作者分享了为《Logic for Programmers》一书编写的Z3 SMT求解器示例代码。文章从基础数学约束求解、优化年金存款、逆向工程线性同余生成器（RNG），到定理证明和股票交易策略，逐步展示了Z3在软件研究和形式化验证中的实际应用。内容包含大量Python代码片段、工程踩坑经验（如Z3数组理论与Python列表的区别、优化器性能问题）以及对SMT求解器局限性的诚实反思，适合对形式化方法、约束编程和底层算法感兴趣的开发者。
也许注释也应该解释“是什么”
作者反驳“注释只解释为什么，不解释是什么”的主流观点。通过变量命名和代码重构（Extract Till You Drop）两个案例，指出过度追求代码自解释会导致上下文切换成本增加。主张在特定场景下，直接写清楚“做什么”的注释比强行拆分函数或依赖版本控制记录更有效，旨在引发关于代码整洁与可读性的工程实践讨论。
形式化规范包管理器：用Alloy揭示Nix的设计优势
作者使用形式化验证工具Alloy，对包管理器的安装和升级逻辑进行建模。通过逐步构建模型，揭示了传统包管理器在依赖升级时可能出现的依赖断裂问题，并展示了Nix如何通过隔离依赖（每个包独立存储其所有依赖）来解决“在我机器上能跑”的问题。文章展示了形式化方法在发现系统缺陷和理解复杂系统设计方面的实际价值。
工程学科能教给我们什么（以及我们能教给工程什么）
本文是跨学科研究项目的第三部分，作者通过采访传统工程领域的从业者，探讨软件工程与传统工程之间的相互借鉴。文章指出，传统工程师在需求分析、前期规划和职业责任感方面优于软件工程师，而软件工程师则在开源社区文化、知识共享以及版本控制工具等方面具有显著优势。作者认为，软件工程应吸收传统工程的严谨性，同时传统工程也可从软件领域引入版本控制和开放协作模式，双方并非对立，而是可以互补。
科学是如何发生的：一场关于编程语言与代码质量的实证研究风波
作者深入复盘了软件工程领域著名的编程语言与代码质量研究争议。文章详细梳理了从原始FSE论文到CACM版本，再到TOPLAS复现研究的完整过程，揭示了数据清洗错误、统计方法缺陷及学术社交机制在科学发现中的作用。对于关注实证软件工程、科研方法论及学术诚信的技术读者而言，这是一篇极具信息量和讨论价值的深度案例解析。
两个工人比一个强平方倍：用PRISM建模任务队列
作者使用概率模型检测工具PRISM对任务队列进行形式化建模，深入分析了吞吐量与延迟的关系。文章指出单Worker时延迟随任务量呈二次方增长，而双Worker能显著降低延迟但吞吐量并非线性翻倍。内容包含具体的PRISM代码实现、数学推导及实验数据，适合对分布式系统理论、性能建模感兴趣的工程师阅读。
A Very Early History of Algebraic Data Types
Been quiet around here! I’ve been putting almost all of my writing time into Logic for Programmers and my whole brain is book-shaped. Trust me, you do not want to read my 2000-word rant on Sphinx post...
滥用Python模式匹配的“罪行”
作者利用Python ABC的subclasshook机制劫持3.10引入的模式匹配功能，实现了非单调类型匹配、字段解构甚至动态组合器。虽然展示了语言底层的黑暗魔法和灵活性，但作者最后明确表示不建议在生产环境中使用。
那些“虽死犹生”的影响力编程语言
作者反驳了将Pascal列为“已死”语言的观点，深入分析了COBOL、ALGOL、APL、BASIC、PL/I、SIMULA 67、Pascal、CLU和ML等历史上重要但如今不再主流的语言。文章详细阐述了这些语言在语法、语义、范式（如面向对象、函数式编程、类型推断）上的开创性贡献，以及它们因过于复杂、缺乏I/O支持、性能问题或商业策略失误而衰落的原因。这是一篇极具信息增量的编程语言历史深度回顾。
Alloy 6：时间算子让并发建模成为可能
作者作为Alloy文档维护者，深入解析Alloy 6版本新增的时间算子（Temporal Operators）如何解决并发建模难题。文章通过具体的代码示例（如小球在图中移动），演示了always、eventually、until等算子的用法，并对比了未来与过去时间算子。作者分享了从TLA+视角转换的经验，指出Alloy 6使形式化验证更易于处理并发系统，但也带来了旧文档过时和新学习曲线的问题。
弱公平与强公平：TLA+并发系统中的公平性解析
作者结合TLA+时钟模型，深入剖析并发系统中的弱公平与强公平概念。通过具体代码示例解释 stuttering 如何破坏活性属性，并对比微软线程调度器的工程取舍，为形式化验证学习者提供清晰的理论到实践的过渡。
Alan Kay 并没有发明对象（2019）
作者通过查阅 Simula 文档、Smalltalk-72 手册及 1981 年 Byte 杂志等一手史料，纠正了“Alan Kay 发明了对象”这一常见误解。文章指出对象概念源自 Simula，Kay 仅创造了术语。同时深入分析了 Smalltalk 与 Simula 在消息传递和运行时绑定上的本质区别，以及两者解决不同问题（个人计算 vs 仿真）的背景，强调现代 OOP 是多方思想的综合。
一个令人困惑的JavaScript解析谜题
文章通过一个JavaScript代码谜题，揭示了-->在行首被解析为注释的遗留特性，并解释了其源于Netscape Navigator 2的历史原因。
控制层级理论（或如何防止开发者误删生产库）
作者借用工业安全领域的控制层级理论，将其映射到软件工程实践中，探讨如何防止开发人员误删生产环境数据。文章从消除、替代、工程控制、行政控制和个人防护装备五个层级进行分析，结合个人踩坑经历和具体技术案例（如权限管理、只读副本、全名确认框等），提出了具有实操性的工程建议，并讨论了控制措施可能引入的新风险。