系统设计两种抽象：Java藏细节 TLA+砍细节 根本两码事！
内容提要
本文区分系统设计中两种抽象：模块化抽象（如Java）通过隐藏内部细节简化使用，建模抽象（如TLA+）通过削减无关信息提炼核心以精确推理。前者隐藏并发，后者暴露并发以验证安全性。工业界如亚马逊已用TLA+发现深层缺陷，但模型回填真实系统仍存挑战。
延伸解读
两种抽象：方向相反，不可混淆
模块化抽象（如Java）通过隐藏内部细节简化使用，而建模抽象（如TLA+）通过削减无关信息提炼核心以精确推理。前者画竖线隐藏并发，后者横切暴露并发以验证安全性。理解这一区别有助于避免将封装误认为建模，从而在系统设计中正确选择方法。
工业界实践：TLA+的价值与局限
亚马逊、微软等公司已用TLA+发现深层缺陷，如亚马逊在DynamoDB中找到一个需35步交错才能触发的bug。然而，谷歌Chubby的经验表明，模型回填真实系统时需补充大量细节，且仍依赖测试。这说明建模抽象虽能发现设计错误，但无法完全替代工程实践。
抽象泄漏：敌人还是原料？
Spolsky的抽象泄漏定律指出模块化抽象会泄漏细节，被视为敌人。但建模抽象却将泄漏视为原料，如逻辑时钟正是利用顺序关系的泄漏来建模。这一对比揭示了两种抽象对细节的不同态度，帮助读者理解为何同一现象在不同视角下意义迥异。
Q&A
系统设计中的两种抽象分别是什么？
系统设计中的两种抽象是模块化抽象和建模抽象。模块化抽象通过隐藏内部细节来简化使用，例如Java中的封装；建模抽象通过削减无关信息来提炼核心，以便进行精确推理，例如TLA+。
模块化抽象和建模抽象在并发处理上有何不同？
模块化抽象（如Java）通过synchronized等机制隐藏并发细节，使调用者看不到中间状态；建模抽象（如TLA+）则故意暴露并发的所有交错，通过模型检查器穷举所有可能，以验证系统不变量。
TLA+在工业界有哪些实际应用案例？
亚马逊在DynamoDB、S3、EBS等系统中使用TLA+，发现了深层缺陷；微软Azure Cosmos DB用TLA+建模一致性语义，找到了持续28天故障的根本原因；此外，MongoDB、Oracle Cloud、谷歌、LinkedIn、Datadog、英特尔等公司也在使用TLA+。
什么是抽象泄漏定律？它与两种抽象有何关系？
抽象泄漏定律由乔尔·斯波尔斯基提出，指所有不平凡的抽象在某种程度上都会泄漏内部细节。该定律主要针对模块化抽象，如TCP、虚拟内存等。而建模抽象则把泄漏视为原材料，利用泄漏的细节进行建模。
为什么说Paxos同时体现了两种抽象？
Paxos的共识规格既是建模抽象砍出来的骨架，用于推理，也是工程师实现时的接口，用于封装。但两种抽象的动作不同：建模抽象是削减，模块化抽象是隐藏。Paxos的产物可以同时服务两个目的，但动作本身不互相转化。
为什么大多数工程师难以掌握建模抽象？
因为计算机专业教育主要教授模块化抽象，如ADT、接口、分层，核心是隐藏细节。而建模抽象的核心是削减无关细节，需要判断哪些是正交的、可安全砍掉的，这需要扎实的领域知识和设计直觉，且编程语言本身无法在代码层面之上做抽象，必须用数学语言。
在写TLA+模型前，应该做哪三个动作？
三个动作是：1. 用一句话写下要保证的性质，然后逐个变量问删掉它是否影响性质判断，不变就删；2. 把模块边界当实现工具，建模时允许跨层横切；3. 故意把并发写成“或”，拆到最小粒度，让TLC穷举所有交错。
建模抽象在真实系统回填时面临什么挑战？
砍到最小的骨架落回真实系统时，需要加入磁盘损坏处理、主节点租约、快照、成员变更等机制，这些不在被证明过的骨架里，导致系统仍依赖大量测试。谷歌Chubby的经验表明，证明过的算法只是起点，回填的每一块可能都需要单独建模，但尚无公认答案。
