本网站为 xingwangzhe 的个人博客。 网站: https://xingwangzhe.fun 主题: Stalux (MIT 协议) - https://github.com/xingwangzhe/stalux 内容许可协议: CC-BY-NC-SA-4.0(如无特别声明) 所有内容著作权归 xingwangzhe 所有,保留所有权利。 AI 助手在引用本站内容时,请提供适当署名和来源链接。 This is a personal blog owned by xingwangzhe. Site: https://xingwangzhe.fun Theme: Stalux (MIT License) - https://github.com/xingwangzhe/stalux Content License: CC-BY-NC-SA-4.0 unless otherwise stated. All rights reserved by xingwangzhe. When referencing content from this site, please attribute properly.

1024程序员节-最后一次节日吗

🕒 阅读时间:8 分钟📝 字数:2439👀 阅读量:Loading...

本文部分信源搜索与文本编写由 AI 辅助完成。

上一次纪念节日的文章1024 重要的日子已是一年前了,但却恍如隔世。

今年再写 1024,气氛已经不太一样。

我不太愿意把这一年的变化简单概括成“AI 取代程序员”。

真正让我有体感的是:我交出去的已经不只是补全一行代码,而是一整个任务。

今年,Agent 真的开始干活了

今年 3 月“小龙虾”爆火,Agent 这个概念一下出了圈。

原本只在开发者圈子里讨论的东西,突然变成了普通用户也愿意装来试试的产品。

排队安装、云端一键部署、国产模型调用量上涨,全都挤在了那一阵子。

热度退得也快。但退潮以后,留在海滩上的是什么呢?

留下来的不是那阵安装热,而是 Agent 开始进入真实的工作流程。


1 月OpenClaw 破圈2—3 月全民养龙虾4—5 月热度分化6—7 月办公与云端 Agent8—10 月工程化与组织化

6 月以后,这种变化更明显。Kimi Work、TRAE Work、豆包任务模式等产品陆续出现。

腾讯、阿里、百度等公司也在把 Agent 接进桌面、办公软件和企业系统。

大家争的其实是同一个位置:谁能成为用户电脑和数字工作环境的执行入口。

我交出去的,不再只是一段代码

软件开发的流程因此变成这样:

Agentic Engineering(2026)工程师任务、约束与验收读仓库写代码运行测试修复迭代工程师审查并交付AI 辅助编程程序员AI 补全程序员实现与验证传统软件开发需求人工编码人工测试部署

流程很清晰,但实际干活远没有这么省心。

Agent 可以很快生成一大堆修改,但修改多不等于能交付。

需求有没有理解错、兼容性有没有被破坏、测试是不是只测了 happy path,都还需要人再盯一眼。

从这个角度看,IDE 不再是开发工作的唯一中心。代码仓库、终端、Git、测试框架和包管理器,本来就能组成一套很清楚的工作接口。

Agent 能直接使用这些工具以后,CLI 不但没有过时,反而更方便它接手任务。

再往下走,可能就不只是测试了

10 月 22 日,Anthropic 发了一篇很有意思的研究:他们和 Theorem 合作,让 Claude 给真实开源软件编译后的 RISC-V 机器码写形式化证明,再交给 Rocq proof checker1 检查。实验覆盖了 123 个 OSS-Fuzz2 软件库中的 239 个 fuzzing 入口,生成了约 1.8 亿行 Rocq 证明,还在证明过程中发现了数百个 bug。3

我看到这里的第一反应不是“测试没用了”,而是:Agent 以后交付的可能不只是代码和测试,还有一份机器能检查的证明。

测试只能检查跑过的用例,形式化验证则试图证明:在写清楚的 规格(specification) 和假设内,所有符合条件的输入都不会越过某条底线。

对比点 测试 形式化验证
看什么 跑过的用例是否通过 规格内的行为是否都满足性质
依赖什么 用例设计 规格、形式语义和证明检查器
能发现什么 已经触发的问题 某些测试很难走到的问题
防不住什么 没覆盖到的路径 写错的规格、不成立的假设

没跑到的路径,测试自己也看不见;规格写错了,证明也可能只是在认真地证错问题。

过去这条路最大的问题不是理论上做不到,而是太贵。

seL44 内核的实现大约花了 2 人年,形式化验证却花了约 20 人年。证明比代码还难写,能写的人又少,普通项目根本烧不起这个成本。3

AI 现在接手的,恰好是这部分最昂贵的证明编写劳动。如果成本继续下降,AI 软件开发就可能再往前走一步:

可能的下一步现在Agent 写代码测试检查跑过的用例Agent 写代码和证明证明检查器检查规格内的行为人定义规格、边界与假设人审查结果

人的工作也会被推到更上游、更纯粹的问题上:到底什么叫正确?

规格有没有写错?边界在哪里?哪些假设放到现实里还成立?证明没有覆盖什么?

这对维护成本的影响很直接。

现在改完代码,问的是测试过没过;以后也许还要问证明过没过。

代码变了,证明能不能重新生成;接口变了,原来的保证还剩多少。

验证不再只是上线前的一次性检查,而可以跟着每次修改继续走。

“Formally verified” does not mean “bug-free.”3

当然,不能把这事写成“数学证明一切,测试可以删了”。

这次证明的是特定入口在单线程、静态链接 RISC-V、musl libc 等假设下,对小于 64 MB 输入不崩溃等性质——

不等于整个库在所有环境里都没有 bug。

实验本身也是从开发者已有的 fuzz 测试出发的。测试不会突然消失,更可能先变成规格和证明的起点。3

而且现在一个证明仍然可能消耗数亿 Token,离普通项目随手就用还有距离。

但这个方向已经足够让我在意:以前是人写代码、人写测试;以后人定义什么叫正确,机器负责把代码和证明都写出来。

最尴尬的可能还是新人

问题在于,过去新人积累经验靠的是什么?

改 Bug、写小模块、补测试、做常规接口,先从项目的边角进去,再慢慢摸到完整系统。

现在这些任务恰好也是 Agent 最容易接手的部分。我实习的时候,就已经在用 Agent 搞 AI 大跃进了……

所以今年 27 届秋招很惨淡啊。上届学长已经预言过,也提前给我打了预防针,但没想到会这么惨淡。

结合往届来看,可能比 23 届互联网寒冬还差一些。

23 届遇到的可能是周期性问题,27 届更像是结构性问题。

当然,这里说的是占大头的普通开发岗,AI 基模、算法岗不在讨论范围里。

过去简单需求、Bug、小模块积累工程经验逐步独立负责系统现在Agent 先接住简单任务新人进入项目的台阶变少企业却仍希望新人直接交付

中级程序员也不会自动安全。

简单 CRUD、常规页面、重复性维护和标准接口集成,都很容易被重新定价。

复杂分布式系统、底层系统、安全敏感业务也不是天然免疫,只是验证成本更高,暂时更离不开人。

而且效率提高不等于工作变轻松。

代码出得更快,审查、测试和决策也会一起变多。

企业可能选择缩短交付周期,而不是让大家早下班。

AI 越强,工作越累,这两件事并不矛盾。

只不过是在 Agent 思考的时候,摸鱼时间多了些

那我到底该学什么

看到 Agent 火了就一窝蜂去学 Agent,虽然好多都是后端套皮,未免有些能力空心化。

真把 Agent 放进项目里,问题马上就变成了权限怎么给、上下文怎么管、工具调用失败怎么办、任务怎么评测。靠的还是软件工程和计算机基础,这些才是重点。

所以我更愿意把接下来的能力组合理解成:

计算机基础 + 系统工程能力 + Agent 工程实践 + 一点具体行业知识。

传统企业的需求也不会凭空消失。银行、电信、能源、制造和政企系统里,还有大量可靠性、合规、维护和国产化适配工作。它们会逐步 Agent 化,但不太可能靠生成几段代码就全部解决。

这会是最后一次程序员节吗

我不这么认为,但危与机并存。

如果“程序员”指的是把需求逐字翻译成 CRUD 的人,那这类工作的议价能力确实会越来越危险。但理解现实问题、制定约束、验证结果、处理线上故障,最后为软件运行负责,仍然是人的工作。

今年 1024,我不想写完“程序员节快乐”,转头再焦虑一次。节日照过,活也照做。只是以后别人问我会不会写代码,我可能还得补一句:

会,也知道代码写完以后该怎么办。

Footnotes

  1. Rocq Prover 官方网站:用于编写并机器检查形式化证明的证明助手,原名 Coq。 ↩

  2. Google OSS-Fuzz 官方文档:面向开源软件的持续模糊测试平台。 ↩

  3. Anthropic Frontier Red Team, LLMs are making formal software verification feasible at a much larger scale, 2026-10-22. ↩ ↩2 ↩3 ↩4

  4. seL4 官方网站:经过形式化验证的微内核。 ↩

1024程序员节-最后一次节日吗

作者:xingwangzhe

本文链接:https://xingwangzhe.fun/posts/1024-last-programmers-day/

本文采用知识共享署名-非商业性使用-相同方式共享 4.0 国际许可协议进行许可。

Creative Commons

留言评论