林一二2024年01月24日 14:45
最近在开发比较容易坑钱的系统，费劲写了几个单元测试，上模拟盘测试又出现几个bug。
每到这种情况，我就怀念起在上科大江智浩老师上的软件工程课上，带我们用 MATLAB 里的工具对心脏起搏器程序做形式化验证，并出具代码和形式化工具的一一对应的报告，那是多么安心的体验。
但现在看来那就像是一场梦，到了字节我甚至没怎么写过单元测试，都靠外包员工人力测试（后来要求覆盖率60%，但我也差不多离职了，而且似乎公司也花钱请了测试工程师来帮我们写）。创业后我要求都写测试，但也只能覆盖自己的代码，外部接口调用都是 Mock 的，上线后发现接口有时不返回，与 Mock 的预期不符。
我最近写的是 Python 语言，已经是最接近实验室环境的语言了，都无法享受到那场梦里的感觉。我平时写的是 TypeScript 和 Rust，就更不可能有这么 fancy 的形式化验证库给我用了。或许我中年之前都只能靠写测试，而不能再入形式化验证的梦吧。