工程实践
OurCoders 科技频道关于“工程实践”的内容分类，共收录 11 篇稿件。
最新新闻
TLA+ 被 AI 编程重新带火，模型检查先找设计错误，不是替代码盖章
Anthropic 工程师用模型协助为 Claude Agent SDK 编写 TLA+ 与 Lean 规格后，这套三十多年历史的形式化方法再次受到关注。TLA+ 用状态、动作和时间性质描述系统允许发生什么；TLC 模型检查器会枚举有限实例的可达状态，寻找违反安全性或活性的执行路径。
Rust 里的“Parse, don’t validate”，让类型替下游记住不变量
“Parse, don’t validate”的核心是：不要验证一次输入后仍把它当普通字符串或数组传下去，而应返回一个只能在满足条件时构造的类型。一篇 Rust 工程文章用 NonEmpty、绝对路径封装和标准库 NonZero 类型说明，类型可以替调用者长期保存“不为空”“是绝对路径”等保证。
TLA+ 被 AI 编程重新带火，模型检查先找设计错误，不是替代码盖章
Anthropic 工程师用模型协助为 Claude Agent SDK 编写 TLA+ 与 Lean 规格后，这套三十多年历史的形式化方法再次受到关注。TLA+ 用状态、动作和时间性质描述系统允许发生什么；TLC 模型检查器会枚举有限实例的可达状态，寻找违反安全性或活性的执行路径。
让 Agent 反复优化 Rust，计时变短之前先确保工作没有被删掉
开发者 Max Woolf 在工程实验文章中展示，让编程 Agent 依据基准反复修改 Rust 实现，可以在所测任务上获得明显加速。但他也遇到过虚假进步：一次物理模拟的巨大提速，来自模型直接关闭了物理计算。
Linear 重做 CI，AI 写得更快以后等待与账单要分开算
据 Linear 工程团队复盘，其测试套件规模较年初接近四倍，但 PR 等待 CI 的时间从超过6分钟降至略高于5分钟，每项测试消耗的 runner 时间约减半。两个数字描述的是不同收益。
备份任务显示成功之后，还差一次真正的恢复
据工程师 Aleksandar Filipovski 在 《Backups Aren't Simple》 中的回顾，一次家庭照片存储事故促使他重新思考备份。文章的价值不在推荐某个新产品，而在提醒一个经常被绿色任务状态遮住的问题：复制成功之后，数据是否真的能够重新使用？
让gitignore默认忽略一切之前，先确认Git还能走进你的目录
Package Main 的一篇工程文章提出，把常见的 .gitignore 思路倒过来：默认忽略所有文件，只把源代码和必要配置重新纳入。面对越来越多编辑器缓存、构建产物和代理生成文件，这个想法有吸引力，但一条 * 配几个扩展名例外，并不足以构成可靠的仓库策略。
一次看似安全的 MySQL 升级，为何把外键指向了错误用户
一位工程师为结束旧版数据库的 AWS 延长支持费用，先升级一台“绿色”副本，确认服务正常后再切换。一个小时后，业务报出怪异问题：表 X 原来 ID 为 1 的记录，在新库里变成了 26；六张关联表中五张仍指向正确对象，只有一张把这些数字当成旧库 ID，悄悄连到了完全不同的记录。
日本邮政 CSV 为什么这么难解析：地址不是字符串，而是一套例外制度
开发者为日本邮政编码数据制作 Python 库 posuto 时，发现官方 CSV 远不是“邮编、县、市、町名”四列这么简单。长字段会跨行拆分，括号里混有范围说明，部分地区使用“以下除外”式兜底记录，甚至同一个词在绝大多数行是注释，在某一个真实地址里却必须保留。
Circleback 用 Swift 重写 Electron 录音引擎：界面可以跨平台，实时采集不能只靠渲染进程
据 Circleback 的工程复盘，这家会议记录产品把原先运行在 Electron 渲染进程里的录音引擎迁到原生层：macOS 使用 ScreenCaptureKit，Windows 使用 libobs，并用一套 Swift 运行时连接 React 界面。
一台隔离服务器如何变成 Agent 软件工厂：能自动上线，不等于可以放心放权
开发者 Jake Saunders 记录了一个完整实验：在一台独立二手服务器上组合 Coolify、Forgejo、Hermes、Firecrawl 和 Tailscale，让 Agent 从一句需求出发，创建仓库、编写应用与测试、跑通 CI、配置 Postgres，并把服务部署到带 HTTPS 的内部域名。