ARTICLE · 1061108

何积丰:他花四十年,给中国软件装上一道＂安全带＂

发布时间：2026-09-23 07:50:24 最近访问：2026-09-23 07:50:14

人物：何积丰

地铁准点到站、汽车自动刹车、火箭按轨道飞行——这些事在今天看来理所当然。可很少有人问过：支撑它们的上百万行代码，凭什么可以被信任？上世纪八十年代，这个问题还是一片空白。一位从复旦大学数学系走出来的上海学者，用最抽象的方式给出了回答：他要把"程序"这件事本身，变成一道能够被证明的题目。

作者/柏舟图片/网络

一个把数学带进软件的人

何积丰，1943 年 8 月生于上海，中国科学院院士（2005 年当选），著名计算机软件科学家，华东师范大学终身教授，现任上海华科智谷人工智能研究院院长、国家可信嵌入式软件工程技术研究中心首席科学家。他的身份标签里有三个"第一"：程序统一理论的创立者、数据精化完备理论的奠基者、基于模型的可信软件设计技术的开拓者。近年又多了一个——在国际上率先提出"可信人工智能"，推动全球关注这一议题。他并非计算机科班出身——1965 年从复旦大学数学系毕业。此后一辈子做的事，本质上是把数学的严谨搬进代码的世界：既然数学定理可以被证明，为什么软件的"正确"不能？

一个数学系毕业生的转行

1965 年 2 月，何积丰从复旦大学数学系毕业，一个月后进入华东师范大学工作，成为上海高校第一批从事计算机科学教学与研究的人员之一。1972 年，他参与上海市第一代国产计算机的研制——那成了他从数学转向计算机的真正起点。更大的转折在上世纪八十年代初：他被学校派往美国斯坦福大学、旧金山大学做访问学者，1983 年转入英国牛津大学计算机实验室，任客座教授、高级研究员，一待就是十五年。也是在牛津，他成为一名共产党员。多年后面对记者，他的回答没有一丝迟疑："我 1983 年入党，想法很简单：做共产党员就应该为国家富强多做贡献。"牛津那段岁月是他学术生涯的黄金期。1998 年，英国科学技术委员会给政府的年度报告这样评价："在过去十五年，何积丰是牛津大学程序研究领域取得成功的驱动力。"2001 年，一通来自上海的电话改变了后半程：学校希望仍在国外任职的他牵头组建软件学院。他回来了。从 5 个人的小团队起步，这所学院后来成为国家首批示范性软件学院之一，输送 3000 多名本硕博专业人才；2012 年教育部学科评估中，其软件工程学科位列全国第四。2002 年成为华东师大首批终身教授，2005 年当选中国科学院院士，2019 年受聘同济大学特聘教授。2026 年 4 月的第十九届中国电子信息年会，他担任"交通产业前沿控制技术"专题论坛主席。

他到底解决了什么问题

给程序语言造一本"通用字典"：世界上有几百种程序语言，命令式的、函数式的、逻辑式的，各说各话。要判断一段程序"对不对"，每种语言都得单独建一套理论——在软件开发越来越复杂的年代，这几乎是一场灾难。1995 年，何积丰与图灵奖得主、英国计算机科学家托尼·霍尔合作，提出了程序统一理论，以及连接各类程序理论的数学法则。用大白话说：他们为形形色色的程序语言造了一本"通用字典"，让不同语言写的东西，终于能被放到同一把尺子下衡量。在此之前，1986 年两人还提出了"程序分解算子"，把"规范语言"与"程序语言"看成同一类数学对象，以"关系代数"作为统一数学模型，由此奠定了软件语义理论的元基础。他们合作的英文专著被引用超过 800 次，该理论已被国际公认为研究各类程序语言的标准方法；自 2006 年起，国际上每两年举办一次专题研讨会。

从图纸到工地：证明每一步都没"走样"。写软件有个天然难题：从"要什么"到"怎么写"，中间要经过无数步转换，每一步都可能悄悄偏离最初目标——而且往往直到系统崩溃才被发现。何积丰创建了数据精化完备理论，首次提出数据精化的"程序分解算子"与"上下仿真映照对"方法，在关系代数框架中建立了求解规范方程的演算法则。通俗地说，他给出了一套可证明的"施工监理"：从图纸到工地，每一步都能验算，保证没有走样。这套理论被多种主流开发方法采用：其中 B 软件开发方法成为法国商业工具 Atelier B 的核心技术，被阿尔斯通、西门子等公司用于严格轨道交通软件的开发。国际计算机科学界因此把它誉为"面向模型软件开发的一个里程碑"。

让地铁和飞机背后的代码值得被信任：理论落地，是何积丰最看重的部分。他开拓了基于模型的可信软件开发与验证领域，建立了正确性系统的可证理论与方法，应用于轨道交通、汽车电子、航天控制等安全攸关行业。两个项目就能说清分量：为国产汽车电子操作系统做验证，使之通过欧洲认证并实现出口；为航天领域研发嵌入式系统需求分析技术，用于重要型号的软件开发。他早年开创的关系程序设计语言，被欧洲计算机界视为继过程语言、函数程序、逻辑程序之后的第四类程序语言的先驱，被赞为"软件设计技术上的一座里程碑"。

问题换了，方法没换：当人工智能呼啸而来，这位研究了一辈子"软件能不能被信任"的学者，转向了同一个问题的新版本：机器能不能被信任。他率先提出"可信人工智能"概念。面对大模型的安全议题，他的分析很冷静：人类如何应对一个可能比自己更强大的智能？大模型"无孔不入"，一旦出了安全问题，影响难以预估。他给出的路径是"对齐"——让系统目标与人类价值观保持一致。他也不回避难点：人类价值观本身多元且动态变化，而对齐需要标杆；模型的"有用性"与"无害性"之间天然冲突。在 2026 年初的一场演讲中，他进一步主张：面对技术滥用、算法偏差、模型幻觉等挑战，需技术创新与制度规范双轮驱动，构建体系化的安全治理框架，为技术发展划定边界。

同行怎么评价他

来自国际同行的评价，往往比奖章更能说明分量：图灵奖得主托尼·霍尔："何积丰教授在极具应用前景的重要领域中的计算科学方面做出了大量的基础性贡献。"图灵奖得主迪杰斯特拉："我发明的关系演算工作主要归功于何积丰的研究。"英国皇家工程院院士麦克德米德（约克大学荣誉博士授予仪式上）："何积丰在软件工程的科学理论与工业实践方面做出了奠基性的工作。"荣誉清单同样厚重：以唯一完成人获国家自然科学二等奖、上海市科技进步一等奖，以第一完成人获上海市科技进步特等奖；两次获英国女王先进技术奖、法国国家棕榈教育骑士勋章；2013 年获何梁何利基金科学与技术进步奖。

每天早上八点半

若只挑一个画面来认识何积丰，我会选这个：只要不出差，每天早上 8 点 30 分，他会准时出现在华东师大中北校区的研究室，一直工作到傍晚 6 点。年过七十时如此，八十岁以后依然如此。他的自我评价低得惊人："我这个人算不上聪明，唯一的诀窍就是每天都不脱离专业工作。"对学生，他有一套近乎"不近人情"的规矩：再优秀的学生，他都"不允许"留在自己身边。多位博士生毕业后被送出国门，分赴昆士兰大学、新加坡国立大学等海外名校做博士后研究。他的理由是——年轻人该去更远的地方看看。但另一面是，他记得每一个细节：每年中秋，他把家里的月饼送到学生宿舍；每年春节，他和留校学生一起吃年夜饭；每年暑假，他带头放弃休息创办暑期学校在华东师大，他为全校本科生开设了第一门由院士独立主讲的通识课"计算机文化"，教室里常常坐不下。而在他所有故事里流传最广的那一个，发生在家里。上世纪八十年代初，他刚被派往美国进修，留守上海的妻子张蕾蕾在一起意外事故中双目失明。为了不影响他的学业，妻子执意让家人隐瞒，家书里只说自己"手骨折了"。得知真相后，妻子写信提出离婚。他立即回信，那几句话被媒体记录了下来："我和你离婚，道义上不允许，感情上不可能。我决不会丢弃你的！"此后几十年，他成了妻子的眼睛。第二次赴牛津时，他把妻子带在身边；每个周末去实验室都带上她，自己埋头研究，妻子在一旁做针线活儿或学英语。他说过一句更朴素的话："没有妻子，我什么也做不了。虽然她失明了，但是我更离不开她。"2005 年，他当选院士的同一年，获评"感动上海十大人物"，有学生在校园论坛上留言："我们又相信爱情了。"对他而言，名字早就写好了答案——只有长期的"积"累，才能获得"丰"收的喜悦。

进步一小点

今天，软件已经渗进生活的每一道缝隙，而人工智能正在把它推进更深一层。半个世纪前何积丰追问的问题——我们凭什么相信一段代码——如今变成了每个人都要面对的追问：我们凭什么相信一个会思考的机器。问题换了，方法没换。他的答案始终如一：把担心变成可以证明的东西。不靠感觉，不靠口号，靠一步一步演算出来的正确性。被问及"中国梦"时，这位院士的说法没有一点豪言壮语："科研人员的中国梦，就是让中国在专业领域站上国际前沿。不要大声喊口号，只要每年进步一小点。"八十三岁这年，他大概还是早上八点半到研究室。每年进步一小点，四十年下来，就是一座里程碑。