Sean Allen：从设计开始保证软件正确性

Sean Allen 说，测试是实现目标的手段：它能做到很多事，但在开发流程中出现得相对较晚。现有工具无法提供完全保证，因此无论团队是否承认，也都在生产环境中测试。

Allen 最初更在意音乐，而不是科技职业。大学毕业后，他搬到纽约，在 Scholastic 找到维修电脑的工作；朋友提到一家初创公司的机会后，他又学习了 Perl。公司虽然倒闭，他却发现自己喜欢编程。少年时他也曾为了制作游戏，尝试阅读一本 Commodore 64 机器语言书。

在 Antithesis，Allen 从事发现软件系统故障的工作。他介绍了一支使用公司产品、挑战产品假设的内部红队，帮助开发者直接了解用户可能遇到的问题。

Allen 看重 OCaml 及相关语言，因为类型系统让开发者能够描述数据可能的形态和状态。编译器随后可以在运行前指出程序没有处理的情况，而不必完全依赖测试人员记住每一种情况。

和类型可以声明一个值属于几种可能情况之一。代码处理这些情况时，编译器可以警告遗漏；新增一种情况后，它也能指出哪些地方需要修改，而不是等到程序运行时才发现。

Allen 对比 C 和 Ada：有些程序在 C 中能通过编译，却会被 Ada 编译器拒绝。当他认识到被拒绝的代码可能造成不安全的内存访问、崩溃等故障时，最初的挫败感发生了变化。

F# 将类似的函数式编程思想带入 .NET 世界。吸引 Allen 的并非某一种语言潮流，而是让编译器帮助维护程序应该具备的性质。

Pony 将面向安全并发的类型系统与 actor 模型结合起来。相互独立的 actor 通过消息通信，而不是让线程任意共享可变状态；语言本身替程序员确定了许多并发规则。

并发错误很难排查，因为每次运行的任务顺序都可能不同。Allen 看重语言层面的保证：它能排除某些数据竞争，而不是要求开发者事后找出每一种有问题的交错顺序。

Erlang 和 Elixir 用户熟悉 actor 模型。Allen 说，Pony 将异步编程与类型系统结合，并提供一套相互配合的机制，而不要求开发者自行拼装并发模型的每个部分。

主持人问垃圾回收为何有速度慢的名声。Allen 区分了回收不再使用的内存这一目标与人们熟悉的具体实现：暂停整个程序会损害尾部延迟，但这不是回收内存的唯一方法。

即使应用自己管理内存，也常常先申请大块内存再切分，例如使用 arena 或 slab 分配器。它们仍需要规则判断内存何时不再使用；内存管理的权衡包括由谁、在什么时候做出这个决定。

Allen 用一个简化模型解释：可以想象每个 Pony actor 都有自己的堆，并负责回收自己使用的内存。程序可以在工作与局部回收之间切换，而不必暂停整个程序。他强调，独立堆只是便于理解的近似说法。

这种方法可能带来更平稳的延迟，代价是峰值吞吐量可能低于把回收推迟的系统。关键区别在于不同的回收策略，而不是垃圾回收与完全没有内存管理成本之间的区别。

Allen 大致将正确性定义为程序按照作者预期运行。他常用“不变量”描述必须持续成立的性质。团队因此需要说清软件应当做什么，包括运行不正常时的预期。

测试对验证很有用，但 Allen 认为改善正确性的第一个机会更早就出现了。如果语言能够表达允许的状态和状态转换，就可以让某些非法状态无法表达，缩小后续测试需要调查的范围。

Allen 喜欢用测试驱动开发设计 API：先写测试迫使开发者使用接口。但对于基于示例的测试，程序可能只是把示例答案写死，也能通过测试。

Allen 说，在结对练习中，只要写死答案能通过现有测试，他就会故意这样做。搭档最终不得不改变或随机生成输入，转向基于性质的测试：针对许多生成的情况检查一条规则，而不是只检查少数选定示例。

职业生涯早期，Allen 喜欢动态语言，认为自己不太需要编译器帮助。随着系统和团队规模扩大，他开始重视即使很基本的编译器反馈，例如删除一个类后指出所有受影响的位置。

Allen 说，对较大的系统而言，测试工作负载包括输入、执行的操作，以及判断结果是否有效的检查。例如测试键值存储时，需要选择读取、写入和删除操作，也需要决定键和值的大小。

仅有随机性并不能保证工作负载有用。如果读取、写入和删除概率相同，连续大量写入、填满存储并触发淘汰或重新分片的情况可能极不容易出现，测试因此永远到不了那些行为。

工作负载应当有意识地把系统推向设计者关心的情况。生成输入的方法和判断结果的规则都需要认真设计：产生大量活动不等于知道观察到的行为是否正确。

Allen 不认同把质量视为开发末尾的一道关卡。代码审查、自动检查和预发布环境都能增加信心，但通过这些环节并不能证明代码在未来遇到的每种情况下都会正常工作。

主持人介绍了分层模型：不同检查发现不同问题。Allen 同意检查有帮助，但认为没有哪一层能堵住所有漏洞：生产环境可能包含测试生成器从未产生过的特殊数据或组合。每个人都在生产环境中继续学习。

按 Allen 的经验，交付可靠的团队在开始设计时就会问：怎样才能知道系统正常工作？对于分布式数据库，这可能意味着检查共识设计或测试早期实现，因为此时修复错误相对便宜。

主持人用搜索排名提出质疑：不同的人可能对哪个结果应该排第一有合理分歧。Allen 将相关性与较简单的性质分开，例如查询是否返回结果、一个用户是否错误收到另一个用户的结果。

即使最佳排名具有主观性，也可以在高负载和并发请求下测试这些性质。给每个查询关联标记，有助于检查服务器是否把正确的响应返回给正确的请求者。

供应链安全涉及系统依赖的组件，而不只是开发者自己写的代码。Allen 说，攻击者可能针对薄弱依赖或构建系统；在持续集成环境中执行的代码可能接触用于发布软件的密钥。

主持人列出可能的缓解措施：延迟更新软件包、移除依赖或维护私有分支。每种方法都有成本；延迟更新也可能延迟安全修复，而如果所有人都等待，仍需要有人发现恶意更新。

Allen 说，常用语言大多赋予导入代码与应用自身类似的广泛能力。一个本来只负责处理文本的小包，可能也能建立网络连接或执行其他计算，这使庞大的依赖树难以审核。

他指出对象能力是一个研究方向：代码要执行建立网络连接等操作，应该先获得明确授予的能力。但如果代码仍可进入不受限制的原生代码，这道边界就可能失效，因此周边系统也很重要。

Allen 把安全问题联系到处理器侧信道。推测执行可以提高处理器速度，但推测路径上的工作有时会泄露信息。他说，自己在 Microsoft 从事机密计算时，安全保证会附带关于侧信道攻击的保留条件。

机密计算的目标是在无需完全信任底层环境运营者的情况下运行软件。Allen 描述的风险不仅包括云服务商恶意行动，也包括员工遭到入侵或贿赂。

他描述了推测执行中的安全与性能权衡：禁用或缓解相关功能可能带来成本，而新的侧信道仍在被发现。Allen 自己也利用处理器行为加速代码，这体现了他所说的权衡。

谈到技术债务，Allen 仍坚持自己早年的观点：并非每个捷径最终都必须偿还。产品可能被停用、业务可能改变，或者替代技术可能让原来的限制不再重要。

他举例说，一个数据库扩展限制曾通过付费使用分布式数据库绕开。新系统需要花钱，而且与单节点方案相比存在一些罕见边界情况；团队根据自身情况认为这些代价可以接受。

主持人回忆了 Uber 成熟的出行业务团队与早期产品团队之间因眼前优先事项不同而产生的摩擦。Allen 认可初创团队有时必须快速行动，但认为容易移除的临时方案与随着其他工作堆积而困住团队的方案不同。

所谓慢下来才能更快，是指先花时间规划、就团队要构建的东西达成一致、决定如何测试，并在完整实现前探索未知部分。Allen 也把疲劳时停下来算在内：疲惫的开发者可能把时间都花在寻找错误上，而非交付有用的功能。

常见的时间浪费来自人们使用相同词语却表达不同意思。Allen 回忆分布式系统中关于“恰好一次”的争论：一方指消息只产生一次效果，另一方指消息在物理上只到达一次。

花几天写清复杂系统应该做什么，可以在修改成本仍然很低时暴露分歧。规划还应询问如何观察生产环境中的系统，包括服务看似仍在线、用户体验却很差的部分故障。