---
title: 1024程序员节-最后一次节日吗
tags:
  - "1024"
  - 程序员节
  - ai
  - agent
categories:
  - 胡思乱想
date: 2026-10-24 12:55:00
desc: 今年再写1024，Agent已经不只是补全代码，而是开始接手完整任务。小龙虾退潮以后，留下的是开发流程的变化：测试、形式化验证、规格定义和维护方式都在重新组合。对新人来说——程序员节确实多了点现实味道。
abbrlink: 1024-last-programmers-day
---
> 本文部分信源搜索与文本编写由 AI 辅助完成。

上一次纪念节日的文章[1024 重要的日子](https://xingwangzhe.fun/posts/749956b2/)已是一年前了，但却恍如隔世。

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

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

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

<!--more-->

## 今年，Agent 真的开始干活了

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

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

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

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

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

---

```mermaid
flowchart LR
    A["1 月<br/>OpenClaw 破圈"] --> B["2—3 月<br/>全民养龙虾"]
    B --> C["4—5 月<br/>热度分化"]
    C --> D["6—7 月<br/>办公与云端 Agent"]
    D --> E["8—10 月<br/>工程化与组织化"]
```



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

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

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

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

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

```mermaid
flowchart TD
    subgraph A["传统软件开发"]
        direction LR
        A1["需求"] --> A2["人工编码"] --> A3["人工测试"] --> A4["部署"]
    end

    subgraph B["AI 辅助编程"]
        direction LR
        B1["程序员"] --> B2["AI 补全"] --> B3["程序员实现与验证"]
    end

    subgraph C["Agentic Engineering（2026）"]
        direction LR
        C0["工程师<br/>任务、约束与验收"] --> C1["读仓库"]
        C1 --> C2["写代码"]
        C2 --> C3["运行测试"]
        C3 --> C4["修复迭代"]
        C4 --> C2
        C4 --> C5["工程师审查并交付"]
    end

    A --> B --> C
```

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

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

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

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

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

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

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

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

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

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

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

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

seL4[^sel4] 内核的实现大约花了 2 人年，形式化验证却花了约 20 人年。证明比代码还难写，能写的人又少，普通项目根本烧不起这个成本。[^formal-verification]

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

```mermaid
flowchart LR
    subgraph Now["现在"]
        direction LR
        A["Agent 写代码"] --> B["测试<br/>检查跑过的用例"]
    end

    subgraph Next["可能的下一步"]
        direction LR
        C["Agent 写代码和证明"] --> D["证明检查器<br/>检查规格内的行为"]
    end

    E["人<br/>定义规格、边界与假设"] --> A
    E --> C
    B --> F["人审查结果"]
    D --> F
```

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

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

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

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

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

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

> *“Formally verified” does not mean “bug-free.”*[^formal-verification]

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

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

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

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

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

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

## 最尴尬的可能还是新人

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

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

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

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

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

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

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

```mermaid
flowchart LR
    A["过去<br/>简单需求、Bug、小模块"] --> B["积累工程经验"]
    B --> C["逐步独立负责系统"]
    D["现在<br/>Agent 先接住简单任务"] --> E["新人进入项目的台阶变少"]
    E --> F["企业却仍希望新人直接交付"]
```

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

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

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

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

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

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

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

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

## 那我到底该学什么

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

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

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

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

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

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

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

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

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

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

[^formal-verification]: Anthropic Frontier Red Team, [LLMs are making formal software verification feasible at a much larger scale](https://www.anthropic.com/research/formal-verification), 2026-10-22.
[^rocq]: [Rocq Prover 官方网站](https://rocq-prover.org/)：用于编写并机器检查形式化证明的证明助手，原名 Coq。
[^oss-fuzz]: [Google OSS-Fuzz 官方文档](https://google.github.io/oss-fuzz/)：面向开源软件的持续模糊测试平台。
[^sel4]: [seL4 官方网站](https://sel4.systems/)：经过形式化验证的微内核。


---

**作者：**xingwangzhe

**本文链接：**[https://xingwangzhe.fun/posts/1024-last-programmers-day/](https://xingwangzhe.fun/posts/1024-last-programmers-day/)

本文采用[知识共享署名-非商业性使用-相同方式共享 4.0 国际许可协议](https://creativecommons.org/licenses/by-nc-sa/4.0/)进行许可。