守株阁

Resharding 是分库分表架构绕不过去的难题。系统上线时用 uid % 2 把数据分到两个库，跑了两年发现容量不够，要扩成四个库——uid % 4。这个 % 号一变，大约 75% 的数据需要重新搬家。搬数据本身不难，难的是三件事同时做到：在线搬、搬完瞬间切、切坏了能回滚。 下面从最朴素的双写到 Vitess 的 VReplication，逐一拆解业界主流的 resharding 在线切换方案。核心问题只有三个：数据怎么不丢，流量怎么瞬间切，故障怎么秒级回。 问题的本质：hash mod 变化引发的数据海啸 hash 取模是最常见的分片路由策略。uid % N 的 N 一旦改变，绝大部分数据的归属分片都会变。 以 2 库扩 4 库为例：原先 uid % 2 = 0 的数据全在 A 库，扩容后 uid % 4 把这批数据拆成了 uid % 4 = 0（留 A 库）和 uid % 4 = 2（搬到新 C 库）。B 库的情况类似，一半数据要搬去新 D 库。 12345678910111213扩容前（uid % 2） 扩容后（uid % 4）┌─────────┐ ...

Anthropic 在 claude-quickstarts 仓库中放了一个 autonomous-coding 示例项目。整个项目只有 8 个 Python 文件、约 500 行代码、一条 pip 依赖（claude-code-sdk>=0.0.25），却能驱动 Claude 在多个 session 之间持续工作数小时，从零构建一个带 200 个测试用例的完整 Web 应用。 这个项目的价值不在于它有多复杂，恰恰在于它有多简单。它是 Anthropic 对"长程自主编码的最小可行 harness"的官方回答，每一个设计决策都值得拆开看。 项目全景 12345678910111213autonomous-coding/├── prompts/│ ├── app_spec.txt # 应用规格说明书│ ├── initializer_prompt.md # 初始化 Agent 的 prompt│ └── coding_prompt.md # 编码 Agent 的 prompt├── autonomous_ag...

124 2026 年 5 月，CMU、Yale、JHU、Virginia Tech、Amazon 等九家机构联合发布了一篇 71 页的综述论文《Agent Harness Engineering: A Survey》。19 位作者对 170 余个开源 Agent Harness 项目做了系统编码，提出了 ETCLOVG 七层分类框架，并给出了一个在业界讨论中反复出现但缺少严格证据支撑的判断：制约 Agent 可靠性的瓶颈不在模型，而在模型外面那层工程系统。 Harness 改一改，性能翻几倍 论文引用了一组对比实验：把 GPT-5.2-Codex 固定不动，只修改 Harness 层——重写系统提示词、加入中间件上下文注入、增设自验证钩子——Terminal-Bench 2.0 得分从 52.8% 升到 66.5%。进一步用自动化 Meta-Harness 优化器调参，分数到了 76.4%，超过人工调优的最好成绩。 另一组实验更激进：仅修改 edit-tool 的格式协议和工具调用规范，编码基准测试的改善幅度达到 10 倍。 这些数字说明的事情很简单：很多团队在抱怨"...

一个项目目标听起来不复杂：把一个已经在线上跑的「客资诊断」agent 系统，用新的技术栈复刻一遍。原系统能根据一个业务 ID 把整条链路的状态查清楚：数据有没有入库、短信发没发、有没有回访，然后给一线同学一份诊断报告。 真正的难度集中在一处：新系统接的工具语义接近、定位接近，但签名不保证一致。项目里专门记失败的那个文件 failuremode.md，最终攒了 47 个不同的 FM 编号。这不是 bug 列表，而是「同一个错误以后还会换个皮再犯」的结构性失败模式。下面把它们摊开看：这些坑的形状高度相似，认出形状比记住每一个坑更有用。 为公开发布，所有内部平台名、数据集名、工号、手机号、文档 ID 均已脱敏，换成功能描述。技术含义不变。 先说那个数字 文档头、README、架构说明里都白纸黑字写着「32 FM-* 失败模式库」。实际 grep 一下： 12grep -oE "FM-[A-Z0-9-]+" docs/failuremode.md | sort -u | wc -l# 47 43 个独立的 ## 段落，加上某个大类底下挂的 4 个子类型，一共 47 个...

有些国际政治问题并不缺材料，难在同一段材料被不同的人剪成不同的形状。 “联合国是否认为台湾是中国的一个省”就是这种问题。 一段视频里，央视记者问联合国秘书长发言人：对联合国来说，台湾是不是中国的一个省？发言人回答“是”。另一段视频里，还是相近的问题，还是联合国发言人，回答却绕开了“省”字，只说联合国立场基于 1971 年联大第 2758 号决议。 这两个回答看起来互相打架。一个像是直接确认，另一个像是在回避。 答案要拆开看：联合国大会 2758 号决议的文本说了一件事，联合国秘书处长期执行时又形成了一套更具体的操作口径。前者解决“中国代表权”，后者把台湾作为中国的一部分处理。把这两层混在一起，就会出现各说各话。 最短答案 如果“联合国官方”指联合国秘书处、法律事务厅、条约保存人、统计和术语系统的实际操作口径，那么答案很明确：联合国体系把台湾作为中国的一部分处理，不把台湾视为具有独立于中国的联合国地位。联合国文件里常见的称谓是 Taiwan, Province of China 或 Taiwan Province of China。 如果“联合国官方”指 1971 年联大第 27...

形式化方法导引主线 13 篇结束后，常被问的延伸问题是："Curry-Howard 同构是不是只有’逻辑 ↔ 类型’这两端？"答案是不完全：1980 年前后 Lambek 把这条同构补成了一个三角——加入范畴论作为第三个等价表述。 逻辑、类型论、范畴论说的是同一件事，只是观察镜头不同。这条三角对应被叫 Curry-Howard-Lambek 同构，是任何想往程序语言语义、依值类型基础、同伦类型论方向走的人必须越过的一座山。 本文是系列附录，不属于主线 13 篇，目的是给硕士生指一条范畴论入门的最短路径。不展开范畴论基础，重点把"三角"的形态点清楚。 三角的形态 123456789101112 逻辑 (直觉主义命题逻辑 IPC) /\ / \ / \ / \ / \ / \ / \ / ...

本系列的主线问题是"为什么形式化编译器编译通过就证明命题得证"。从第 00 篇到第 11 篇，答案已经分层给出： 直觉主义逻辑把"证明"重新定义成"构造一个见证物"（第 01 篇）。 Curry-Howard 同构把命题、类型、程序、证明检查四件事压成同一个对象（第 02 篇）。 STLC 是最小可证明系统，能精确表达直觉主义命题逻辑（第 03 篇）。 类型检查算法是机械、可终止、可被任何语言实现的（第 04 篇）。 依值类型把表达力从命题逻辑扩到一阶逻辑（第 05 篇）。 归纳类型让数据嵌入证明，递归即归纳法（第 06 篇）。 Lean 4 把这套机制工程化，环境可在本地或浏览器跑起来（第 07-08 篇）。 可信基底说清了"编译通过"到底信什么（第 09 篇）。 大型案例（CompCert、seL4、Four Color、Mathlib）展示了"能干到多深"（第 10 篇）。 局限与取舍说清了"什么时候不该上"（第 11 篇）。 本篇收束。它要回答两个尾...

第 10 篇展示了 CompCert、seL4、Four Color、Mathlib4、Feit-Thompson 五个把形式化推到极致的项目。它们也共同暴露了一件事：形式化的代价非常高，证明/代码比常在 2-25:1，时间跨度通常以年计，依赖少数 deep expert。 本篇接着这条线，回答"什么时候不该上形式化"。判断的边界与判断的成本本身同等重要：错用形式化的项目要么半途而废，要么变成一份维护负担巨大的"科研作品"。 本篇分四部分：形式化能给的与不能给的、与传统验证手段的关系、典型决策维度、几条可操作的判断准则。 形式化能给的与不能给的 能给的： 对被建模部分的深层正确性保证。证完后该部分的实现错误被排除到内核 + 模型外。 一致的接口：能用同一种语言（Lean / Coq）同时写程序、写规约、写证明、写元理论。 跨变更的稳健性：每次修改 Lean 都重新检查全部依赖；不存在"改完忘补测试导致 regression"这种事。 公开的信任面：通过 #print axioms 与代码评审可精确审计相信了什么。 ...

到第 09 篇为止，本系列把形式化方法的概念骨架、工具操作与可信基底都说清楚了。本篇离开理论，看四个被广泛引用的真实大型形式化项目：CompCert、seL4、Four Color Theorem、Mathlib4。 每个案例按同一个模板梳理： 它证了什么。 代价多大（人月、行数、时间跨度）。 信任面在哪里。 对工程或数学意味着什么。 读完本篇之后，"形式化能在工程里干到多深"这件事不再抽象——四个案例给出了四种不同形态的答案。 CompCert：一个被形式化验证的 C 编译器 证了什么：CompCert 是一个 C 子集（接近 C99，但去掉部分边角语义）的优化编译器，从 C 源代码编译到 PowerPC、ARM、x86、RISC-V 汇编。它在 Coq 里证明了一条语义保持定理： 若源程序 S 没有未定义行为，则编译后的目标程序 T 的所有可观察行为都是 S 的可观察行为的子集。 形式化的"正确"在这里被精确定义成"源语言形式化语义与目标语言形式化语义之间的精化关系"。CompCert 给两端都写了形式化语...

题面 把一个真实落地的项目折叠成一道架构题： 有一个 git 仓库，里面散落着 N 个 SKILL.md 文件（带 YAML frontmatter + 同目录的资源文件）。要做一个内部「Skill Hub」服务： 浏览、搜索、分类、查看详情 在线预览 markdown 与文件树 一键下载某个 skill 的 zip 包 源仓库 push 时 Hub 要自动跟上 部署形态是单 Node 进程（容器平台只给一个端口） 怎么设计？ 约束是分批给的。每听完一版方案，就追加一个新约束逼着方案迭代。下面 14 层按这个节奏走。每层先写最朴素的版本，再写暴露出来的问题，最后写改进，配最小可读的代码片段。 代码片段、字段名、目录名都是从一个真实落地的项目里抽出来的，业务和组织信息已经全部抹掉。 第 1 层：最朴素的版本 最直接的实现： 12345app.get("/api/skills", async () => { await exec("git clone --depth 1 $REPO /tmp/work"); con...