Hillel Wayne

RSS: https://www.hillelwayne.com/index.xml
Hillel Wayne 的技术博客，关于形式化方法、TLA+ 与软件正确性。

形式化地规约 UI

作者 Hillel Wayne 用真实 UI 项目（Edmodo 的 Snapshot 报告页）说明：当界面变复杂后，可以用有限状态机、Harel 状态图（HSC）和 Alloy 形式化规格来捕捉导航逻辑中的隐藏 bug，比如没有起始状态、重复按钮行为歧义、答案报告成为死胡同等。 文章展示了如何把嵌套状态画成简洁 HSC，并用 Alloy 验证"是否必须经过学生页才能到答案页"等性质，还提到 Waterloo 的 DASH 变体为 Alloy 加入了原生 HSM 语义。 作者强调形式方法不只是 NASA/学术工具，对日常 UI 设计同样有价值，哪怕只花几小时画状态图也能在早期发现设计缺陷。文末推广了他的形式方法咨询服务。
评论点赞收藏6 小时前

谓词逻辑速成课

<p>我开始写作因为当时没有适合程序员的好逻辑资源。现在书出版了，新的问题是没有好资源<em>免费</em>为程序员准备的逻辑资源。</p><p>所以，要解决<em>那</em>问题（也许还有点炒作这本书），我把《LfP》的第二章改成了一篇博客文章。所有脚注均为书中未包含的编辑评论。请欣赏！</p><h2>第二章：逻辑速成课</h2><p>形式逻辑是一个非常强大的工具，但它也非常简单。在本章中，我们将激励并解释基本概念和语法。这包括谓词、蕴含算子、集合和集合量词。<br><br>你可能已经通过编程经验熟悉很多内容！</p><h2>谓词</h2><p>从第一近似来看，谓词是一个返回布尔值的函数。作为程序员，你可能写过几十个谓词。这些都是谓词：</p><ul> <li><code>Positive(x)</code>当 x 大于 0 时 为真。</li> <li><code>IsSum(x, y, z)</code>如果 x 加 y 等于 z，则为真。</li> <li><code>RAMAtLeast(c, r)</code>如果计算机 成立<code>c</code>至少<code>r</code>物理内存的字节。</li> </ul><p>我说“对第一近似”是因为谓词是一个数学概念，而不是编程构造。程序函数需要附带计算答案的方法，而谓词只是定义答案。取<code>RAMAtLeast</code>：软件实现会依赖于编程语言、操作系统，甚至可能的物理硬件。<br><br>但谓词呢？如果计算机有内存，则为真;没有，则为假。仅此而已。</p><p><strong>这意味着谓词可以比编程函数更抽象，</strong>表达一些我们甚至无法计算，或者至少还不知道怎么计算的事情。这些谓词同样有效：</p><ul> <li><code>CanRunProgram(c)</code>如果计算机 成立<code>c</code>能够运行我们的程序，无论“有能力”最终意味着什么。</li> <li><code>RainyDayI…</code></li></ul>
评论点赞收藏29 天前

为什么人们不使用形式化方法？

作者梳理了形式化方法在工程界长期未被普及的历史脉络与核心障碍，指出证明过程的高门槛、规格定义的困难以及性价比问题才是主因。
评论点赞收藏62 天前

程序员的逻辑现已可用

<p>我很高兴地宣布，我的书，<em>程序员逻辑</em>， 现已上市！你可以去看看或者直接去买或.如果你买了抢先体验版本，可以免费从.</p><p>这酝酿已久。形式逻辑是一个极其强大的工具来理解软件。从“什么是左外接合”到“为什么不应该这样”，各种问题都有<code>Square</code>继承自<code>Rect</code>如果你懂一些基础逻辑，这才更合理。<br><br>然而实际上并没有任何专门针对程序员的资源<em>学习</em>那些基础知识。你只是被期望打开数学书，或者通过潜移默化地拿起它。</p><p>渗透法行不通。</p><p>所以我过去五年一直在制作那个资源。<em>程序员逻辑</em>教授在职开发者基础逻辑及其多种应用，涵盖从基于属性的测试、领域建模到逻辑编程等多元领域。<br><br>这本书适合没有数学背景的人：如果你懂 AND 和/或 OR，可以读这本书。我花了几个月时间研究每一章的主题，然后请领域专家审核以确保内容准确，再交给初级程序员审核，确保内容易于理解。</p><p>总之，我很累，也很高兴终于结束了。非常感谢你的阅读，希望你喜欢这本书。</p>
评论点赞收藏63 天前

芝加哥与纽约披萨之争是个伪命题

作者认为芝加哥深盘披萨与纽约薄底披萨属于不同消费场景，不应直接比较。作者提出真正的对标物是纽约披萨与芝加哥热狗，并从便携性、家庭制作难度等角度进行对比，最后延伸至意大利牛肉三明治等其他芝加哥美食。 文章以个人经验和幽默视角解构经典美食争论。
评论点赞收藏134 天前

我们是工程师吗？关于软件身份认同的深度调查

作者通过采访17位从传统工程跨界到软件开发的从业者，探讨软件工程师身份认同问题。文章反驳了软件缺乏数学基础、后果不严重或无需执照就不是工程的观点，指出传统工程界内部定义也模糊，多数跨界者认可软件工程的工程属性，并区分了软件开发与软件工程的差异。
评论点赞收藏211 天前

一些有趣的 Z3 脚本评论汇总

作者 Hillel Wayne 汇总了此前发布的 Z3 脚本文章收到的读者反馈、相关博客链接及邮件评论，属于社区互动内容的整理。
评论点赞收藏215 天前

我写的一些Z3求解器趣味脚本

作者分享了为《Logic for Programmers》一书编写的Z3 SMT求解器示例代码。文章从基础数学约束求解、优化年金存款、逆向工程线性同余生成器（RNG），到定理证明和股票交易策略，逐步展示了Z3在软件研究和形式化验证中的实际应用。 内容包含大量Python代码片段、工程踩坑经验（如Z3数组理论与Python列表的区别、优化器性能问题）以及对SMT求解器局限性的诚实反思，适合对形式化方法、约束编程和底层算法感兴趣的开发者。
评论点赞收藏219 天前

也许注释也应该解释“是什么”

作者反驳“注释只解释为什么，不解释是什么”的主流观点。通过变量命名和代码重构（Extract Till You Drop）两个案例，指出过度追求代码自解释会导致上下文切换成本增加。 主张在特定场景下，直接写清楚“做什么”的注释比强行拆分函数或依赖版本控制记录更有效，旨在引发关于代码整洁与可读性的工程实践讨论。
评论点赞收藏269 天前

形式化规范包管理器：用Alloy揭示Nix的设计优势

作者使用形式化验证工具Alloy，对包管理器的安装和升级逻辑进行建模。通过逐步构建模型，揭示了传统包管理器在依赖升级时可能出现的依赖断裂问题，并展示了Nix如何通过隔离依赖（每个包独立存储其所有依赖）来解决“在我机器上能跑”的问题。 文章展示了形式化方法在发现系统缺陷和理解复杂系统设计方面的实际价值。
评论点赞收藏302 天前

工程学科能教给我们什么（以及我们能教给工程什么）

本文是跨学科研究项目的第三部分，作者通过采访传统工程领域的从业者，探讨软件工程与传统工程之间的相互借鉴。文章指出，传统工程师在需求分析、前期规划和职业责任感方面优于软件工程师，而软件工程师则在开源社区文化、知识共享以及版本控制工具等方面具有显著优势。 作者认为，软件工程应吸收传统工程的严谨性，同时传统工程也可从软件领域引入版本控制和开放协作模式，双方并非对立，而是可以互补。
评论点赞收藏317 天前

科学是如何发生的：一场关于编程语言与代码质量的实证研究风波

作者深入复盘了软件工程领域著名的编程语言与代码质量研究争议。文章详细梳理了从原始FSE论文到CACM版本，再到TOPLAS复现研究的完整过程，揭示了数据清洗错误、统计方法缺陷及学术社交机制在科学发现中的作用。 对于关注实证软件工程、科研方法论及学术诚信的技术读者而言，这是一篇极具信息量和讨论价值的深度案例解析。
评论点赞收藏331 天前

在J语言中手写程序

作者尝试用手写方式编写J语言代码，发现J语言的隐式语法本质是二叉树，通过手绘树结构能更直观地理解和编写复杂的J代码，并分享了性能对比和视觉化注释的实验。
评论点赞收藏337 天前

两个工人比一个强平方倍：用PRISM建模任务队列

作者使用概率模型检测工具PRISM对任务队列进行形式化建模，深入分析了吞吐量与延迟的关系。文章指出单Worker时延迟随任务量呈二次方增长，而双Worker能显著降低延迟但吞吐量并非线性翻倍。 内容包含具体的PRISM代码实现、数学推导及实验数据，适合对分布式系统理论、性能建模感兴趣的工程师阅读。
评论点赞收藏346 天前

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...
评论点赞收藏370 天前

滥用Python模式匹配的“罪行”

作者利用Python ABC的subclasshook机制劫持3.10引入的模式匹配功能，实现了非单调类型匹配、字段解构甚至动态组合器。虽然展示了语言底层的黑暗魔法和灵活性，但作者最后明确表示不建议在生产环境中使用。
评论点赞收藏405 天前

那些“虽死犹生”的影响力编程语言

作者反驳了将Pascal列为“已死”语言的观点，深入分析了COBOL、ALGOL、APL、BASIC、PL/I、SIMULA 67、Pascal、CLU和ML等历史上重要但如今不再主流的语言。 文章详细阐述了这些语言在语法、语义、范式（如面向对象、函数式编程、类型推断）上的开创性贡献，以及它们因过于复杂、缺乏I/O支持、性能问题或商业策略失误而衰落的原因。 这是一篇极具信息增量的编程语言历史深度回顾。
评论点赞收藏445 天前

Alloy 6：时间算子让并发建模成为可能

作者作为Alloy文档维护者，深入解析Alloy 6版本新增的时间算子（Temporal Operators）如何解决并发建模难题。文章通过具体的代码示例（如小球在图中移动），演示了always、eventually、until等算子的用法，并对比了未来与过去时间算子。 作者分享了从TLA+视角转换的经验，指出Alloy 6使形式化验证更易于处理并发系统，但也带来了旧文档过时和新学习曲线的问题。
评论点赞收藏495 天前

弱公平与强公平：TLA+并发系统中的公平性解析

作者结合TLA+时钟模型，深入剖析并发系统中的弱公平与强公平概念。通过具体代码示例解释 stuttering 如何破坏活性属性，并对比微软线程调度器的工程取舍，为形式化验证学习者提供清晰的理论到实践的过渡。
评论点赞收藏503 天前

Alan Kay 并没有发明对象（2019）

作者通过查阅 Simula 文档、Smalltalk-72 手册及 1981 年 Byte 杂志等一手史料，纠正了“Alan Kay 发明了对象”这一常见误解。文章指出对象概念源自 Simula，Kay 仅创造了术语。 同时深入分析了 Smalltalk 与 Simula 在消息传递和运行时绑定上的本质区别，以及两者解决不同问题（个人计算 vs 仿真）的背景，强调现代 OOP 是多方思想的综合。
评论点赞收藏511 天前

给非玩家的游戏推荐

作者基于April Cools活动，为不玩游戏的朋友推荐了四款入门游戏：Baba is You、Stardew Valley、The Case of the Golden Idol和Balatro。 文章详细阐述了选品标准（无需特殊硬件、无文化门槛、具有文化意义且经本人验证非玩家喜爱），并深入分析了每款游戏的设计哲学、类型演变及为何适合新手。 内容兼具个人体验、行业观察和具体的游戏推荐，对科技和游戏爱好者有较高参考价值。
评论点赞收藏547 天前

登录芦苇

登录后关注作者、收藏内容和参与讨论。

热门话题

人工智能12,865 人关注AI 会怎样改变日常工作？产品思考8,243 人关注怎样判断一个产品值得长期做？独立开发5,917 人关注一个人如何持续完成作品？
关于芦苇 · 联系我们 · © 2026 芦苇