Assumptions weaken properties2 months agohttps://buttondown.com/hillelwayne/archive/assumptions-weaken-properties/性质/测试的强度通过逻辑蕴含来定义：更强的性质保证更弱的性质。向规约添加假设总会使结果性质变弱，形式化为：Prop ⇒ (Assumption ⇒ Prop)。假设较少的系统更健壮，适用范围更广（例如，Unicode JSON 解析器与仅支持 ASCII 的解析器相比）。依赖假设的三个常见原因：强性质无法实现、成本过高或难以直接验证。大多数假设涉及外部“外程序”因素（环境、硬件、用户输入），这使得它们的验证与系统逻辑的验证截然不同，通常也更困难。
Logic for Programmers extra credits2 months agohttps://buttondown.com/hillelwayne/archive/logic-for-programmers-extra-credits/本周因在布达佩斯参加会议，没有正式的新闻通讯。补充材料撰写了书中未包含的额外主题《程序员的逻辑》。涵盖主题：并发进程的排序计算、一阶逻辑与函数、子类型中的Liskov历史规则，以及全序/偏序关系。补充材料较为粗糙，可能包含错误，但提供了2000-3000字的数学内容。
The Proof Machine (2016)2 months agohttps://incredible.pm/「不可思议的证明机」是一款可视化工具，通过拖拽连接积木块完成命题逻辑、谓词逻辑等逻辑系统的证明。用户添加代表证明步骤的积木块；若结论变为绿色，则表示已构建完整证明。该工具旨在传递计算机辅助证明的乐趣，无需预先了解Isabelle等定理证明器的语法知识。公式输入仅限特定积木块（如¬-块），需使用缩写：&代表∧，|代表∨，->代表→，^代表↑，~代表¬，!代表∀，?代表∃，False代表⊥。当前证明仅保存在浏览器本地存储中，可能丢失；未来计划支持服务器端保存。该工具为自由软件，欢迎贡献；学术细节请参阅相关出版物。