深耕软件形式化理论、执掌北航转型的李未院士

李未（1943年6月8日-2026年1月25日），男，出生于北京市，北京航空航天大学计算机学院教授，博士生导师，中国科学院院士，计算机科学家、教育家，中国计算机和人工智能领域重要奠基人之一，第十、十一届全国政协委员，北京航空航天大学原校长。

作为改革开放后首批公派留英计算机博士，李未一生分为两条主线：一边深耕软件底层数理逻辑，攻克高可靠军用、航天软件理论难题；一边执掌北航七年，推动学校办学定位整体升级，同时深度参与大飞机国家重大专项论证，是空天信息交叉领域标志性学者 。

科研领域，他是国际上较早研究并发程序操作语义的一批学者，针对传统逻辑系统只能处理确定信息、无法应对程序迭代出错、条件不确定的短板，原创开放逻辑理论与R-修正演算体系，建立软件错误定位、版本迭代演化的完整形式化方法，为载人航天、大型客机复杂工业软件筑牢可靠性理论根基 。上世纪九十年代牵头创建软件开发环境国家重点实验室，长期担任863、973计划首席专家，国内最早系统提出海量信息处理研究方向，晚年提出群体软件工程、群体智能概念，研究方向提前契合新一代人工智能发展路线 。

2002年出任北航校长之后，他主导办学思路转型，叫停单纯扩张校区规模的模式，转向质量优先、创新人才培养路线，开创性推行本科生全程导师制，在当时高校圈引发不小讨论；按照一级学科重构院系架构，下放办学权限，重点打造空天信融合特色，让北航综合排名和学科实力迈上一个台阶 。同时受命担任大飞机专项论证专家组组长，为C919立项落地完成关键论证工作 。

任职期间也遭遇重大舆论考验，2004年北航爆出广西招生舞弊事件，牵扯校内教职工与校外利益链条，一度登上焦点访谈。李未第一时间公开认错、承认管理存在漏洞，对涉事人员严肃处理，同步整改招生流程，但这件事也让他的校园管理能力受到不少争议，外界对其管理风格评价出现明显分化 。

学术路线层面同样存在行业分歧。他主攻的形式化逻辑、可信软件方向，理论门槛高、见效周期长，短期很难产出亮眼产业化成果，不少应用领域科研人员认为投入产出比偏低；但在航空航天、军工等不容程序出错的关键领域，这套理论体系不可替代，属于典型“平时不起眼、出事顶大用”的长线基础研究。

卸任校长之后，他依旧深耕教学与学术推广，国内率先发起高校计算机慕课联盟，推动优质线上课程普及，一生累计培养两百多名硕博研究生，拿下国家自然科学二等奖、国家科技进步二等奖等多项重磅奖项 。

放到高校办学与科研选择层面来看，这件事有很现实的思考空间。高校管理者既要抓学科排名、科研产出，又要守住管理纪律、办学口碑，扩张速度和风险管控很难做到完美平衡；科研领域同样如此，愿意长期坚守基础理论冷门方向的学者，在短平快的评价体系里往往不占优势，却能在国家重大工程关键时刻发挥不可替代的作用。

各位读者你们怎么看？欢迎在评论区讨论。