随着大模型与Agent框架的爆发，软件生成的成本正在趋近于零。真正限制 AI 编程落地的瓶颈，正在从“能不能写代码”转向“生成的代码是否正确、可验证、可维护”。

本次演讲将首先回顾Agent智能体在编程领域的技术演进：从代码补全、单文件生成，到当前的多文件修改、工具调用、自主调试，再到未来可能实现的规格驱动开发。在此基础上，重点分析Agent能力发展过程中被忽视的技术瓶颈——不是模型参数量不够大，而是缺乏对生成代码的可验证、可维护、可演化的工程约束。

最后，以IDEA研究院的MoonBit语言作为案例，简要展示一种“面向Agent的编程语言”如何通过语法设计、类型系统、形式化验证接口，让Agent从“写代码的助手”升级为“可信系统的共同构建者”。

演讲提纲：

一、Agent编程能力的真实水位

  - 从Copilot到Devin、SWE-Agent：Agent能做什么，不能做什么

  - 公开基准（SWE-bench等）的局限性与误导性

  - 提出核心问题：为什么Agent写的代码在Demo里惊艳，在真实项目中翻车？

二、Agent技术演进路线：三代能力跃迁

  1、第一代：代码补全 & 单函数生成（2021-2023）

    - 技术特征：基于上下文填充，无规划能力

  2、第二代：多文件编辑 & 工具使用（2023-2024）

    - 技术特征：Agent+检索增强（RAG）+ 简单的错误反馈循环

    - 代表工作：SWE-agent、OpenDevin、AutoCodeRover

  3、第三代：规格约束下的自主构建（2024-现在）

    - 技术特征：Agent读取形式化规格（spec）、生成证明、与验证工具协作

    - 关键进展：自然语言→形式化规约的自动生成（GPT-4o、Claude 3.5等）

    - 技术深度剖析：为什么类型系统、合约、前置/后置条件对Agent至关重要

三、当前技术的瓶颈：从“能写”到“可信”

  1、实证数据：Agent生成的代码在Python/JS等动态语言中的长期维护问题

  2、技术观察：

    → 验证成本远大于生成成本，这是被行业严重低估的瓶颈 

    → Agent缺乏“反事实推理”：能写实现，不能写为什么实现是对的 

    → 真实工程需要：可重现构建、跨环境兼容、团队可读性——这三项Agent几乎都做不到

3、行业探索方向：

    - 基于强类型语言的Agent生成（Rust、Haskell）

    - 引入轻量级形式化验证（Liquid Types、Refinement Types）

    - AI 辅助生成规格（spec）与不变量（invariant）

四、案例：MoonBit如何尝试解决上述问题

  1、MoonBit 的设计目标：面向AI生成+人工审核+自动化验证的编程语言

  2、三个关键技术回应：

    - 面向Agent友好的语法：减少歧义，减少LLM的token浪费，提高生成成功率

    - 一等形式化验证（moon prove）：让Agent可以生成前置/后置条件，自动验证

    - 多后端与可重现构建：解决“在这里能跑，在别处不行”的Agent通病

  3、初步数据：在内部SWE-AGI基准中，可验证代码的接受率提升2-3倍

五、总结与展望：Agentic Software Engineering 的未来

  1、未来的Agent不是更大的语言模型，而是语言模型+验证器+类型系统+构建系统的紧耦合体

  2、编程语言的角色从“给人写”转向“给人+Agent+机器验证器”三方协作

  3、开放问题：规格的自动生成、验证的及时性、人机协同的交互范式

听众收益点：

1、重新理解 Agent 编程的核心瓶颈，听众将看到 Agent 落地的关键问题不是“模型会不会写代码”，而是生成代码如何在规格、测试、类型系统和形式化验证约束下进入真实工程。

2、获得一套 AI 原生软件工程的架构思路，通过 MoonBit 的语言设计、工具链、包管理、SWE-AGI 评测和 moon prove 验证实践，理解如何把 Agent 从“代码助手”升级为“软件构建参与者”。

3、了解可验证代码在 Agent 时代的实际价值，听众可以理解形式化验证为什么会因为 AI 而重新变得实用：AI 降低了写规格和证明的成本，而验证工具负责把“看起来对”推进到“性质上可检查”。