一本面向工作程序员的逻辑学书籍，227 页，无数学背景要求。内容涵盖从"简化条件语句"到"发现并发设计中的竞态条件"再到"最小化分布式任务耗时"。使用英语单词而非数学符号（如 all p in People 而非 ∀p），使形式化方法变得平易近人。覆盖 Dafny、TLA+、Alloy、Prolog 等工具。