国内许多高校的计算机学院都设立了诸如图灵班、ACM 班、IEEE 班等拔尖班级，旨在吸引优秀学生投身计算机科学的学习。这些学生的一大共同特点是他们在进入这些拔尖班级之前就已经具备了扎实的编程基础。如何针对这些基础良好的学生上好计算机学科的第一门课——“计算概论”，成为一个需要认真解决的课题。这里针对北京大学“计算概论”课程的拔尖班情况进行一些简单汇总，希望能对同类教学引发思考。

1 拔尖班“计算概论”课程基本信息

从 2020 年秋季学期开始，我们在北京大学计算机学院开设了“计算概论 A（实验班：函数式程序设计）”。课程目标是培养学生使用函数式思维进行程序设计和推理的基本能力，熟练使用 Haskell 语言进行程序设计，熟练使用 Agda 语言对 Haskell 程序进行推理和变换。课程授课对象为北京大学信息科学技术学院大一新生和高三预科生。课程总计 96 学时：每周 2 次授课（4 学时），1 次上机练习（2 学时）。从开课以来，选课学生逐年递增：2020 年20 人、2021 年 45 人、2022 年 46 人、2023 年 64 人、2024 年 80 人。

开设这门课的主要原因有 4 点：①北京大学信息科学技术学院的大一新生中，有相当比例的学生已经具备了非常强的编程能力；对于这部分学生而言，“计算概论 A”普通班（面向无编程基础学生）的授课内容过于简单，无法为其专业能力的进一步提升提供有效帮助。②函数式程序设计为培养学生的计算思维和形式化思维提供了一个很好的起点；很多国际一流大学也把函数式程序设计作为对本科生开设的第一门程序设计课程。③随着软件技术的持续发展，主流程序设计语言都将函数式程序设计作为其核心语言成分；越来越多的学生开始对函数式程序设计产生浓厚的兴趣。④函数式程序设计为若干后续专业课程的学习打下了必要基础；例如，北京大学计算机学院还开设了面向大三学生和研究生的专业课程“编程语言的设计原理”“软件基础理论与实践”。

课程内容主要包括 3 个方面。①Haskell 函数式程序设计：主要关注如何描述软件做什么（What）；主要知识点包括类型与类型家族、序列操作、递归函数、高阶函数、描述副作用的函数、惰性求值等。②基于 Agda 的程序推理与推导：主要关注如何告诉软件正确且高效地做（How）；主要知识点包括可验证函数式程序设计（基于定理证明器 Agda）、程序演算理论（Bird Meertens Formalism，BMF）、程序推导与程序综合。③信息技术的基础知识，主要知识点包括计算的基本原理、计算机软/硬件基础、程序设计语言、计算机网络等。

根据课程目标和课程内容，我们选取了 3 本专业书籍作为课程教材：①《Programming in Haskell》by Graham Hutton；②《Verified Functional Programming in Agda》by Aaron Stump；③《Lectures on Constructive Functional Programming》by Richard S. Bird。其中，第一本书籍主要关注如何使用 Haskell 语言进行函数式程序设计；第二本书籍主要关注如何使用定理证明器 Agda 对函数式程序进行验证；第三本书籍主要介绍构造型函数式程序设计理论。

2 授课的几点基本原则

简单案例驱动的基本原理讲解。例如，贯穿课程的简单案例之一是“如何构造出一个正确而且高效的计算机程序用于解决最大子段和问题？”。在第一次课上，向学生提出这个问题，根据经验，有很多学生会立刻反馈说“这个问题太简单了”，此时，我们反问学生“如何证明你写出的程序的正确性”。对于大部分具有编程基础的学生而言，“如何用证明的方式证明程序的正确性”这一问题，会对他们产生很大的触动，编程和证明似乎是两件风马牛不相及的事情。以这个问题为牵引，在授课过程中，逐步介绍如何通过高阶函数的组合对该问题进行规约，如何通过构建序列上的演算理论，利用形式化的程序演算理论将该问题的规约（简洁但低效）逐步变换为高效的软件代码。

注重提高授课过程的趣味性，避免照本宣科式的填鸭式教学。在课程幻灯片中，设计“唐僧”和“小和尚”两个角色，其中，唐僧代表啰唆感十足的中老年授课老师，而小和尚则代表具有“初生牛犊不怕虎”特质的青年学生；唐僧与小和尚的对话贯穿在课程幻灯片的各处，用带有一定幽默感的“提问—回答”方式对知识点进行分析和串联，引导学生以一种轻松的方式对相关知识点进行深入思考。

注重提升学生的科研审美能力，鼓励学生进行创新性的科研工作。在授课过程中，通过大量的程序案例对比，展示函数式程序的简洁性和美感。为了解释这种美感的来源，我们用4个学时讲解函数式程序设计与范畴论之间的深刻关系，以及范畴论的核心思想和基本概念。同时，为了激发学生的科研兴趣，还介绍函数式程序设计与数学定理证明之间存在的同构关系（即两者在本质上是相同的），以及函数式程序设计所基于的类型论（Type Theory）的最新进展及其正在对数学领域产生的革命性影响（即将数学的基础从集合论迁移到类型论），进而向学生展望“数学家就是程序员”这样一种看似奇怪却正在真实发生的未来。

3 结 语

在课程的授课过程中，我们内心始终存在一种谨小慎微、如履薄冰的心态。非常欣喜的是学生对这门课的认可程度不断提升，从开始的 8 人报名，到 2024 年 80 人选课。选课学生是全中国同龄人里最优秀的一批青年人。如何将这些学生培养成为对国家的创新型发展起到实质性作用的人才？对于这一问题，我们无法给出明确的答案，只能在实践中不断尝试，持续反思，徐徐前行。

第一作者简介：胡振江，男，北京大学教授，研究方向为程序设计语言，huzj@pku.edu.cn。

引用格式：胡振江,张伟.拔尖班计算概论教学的一点尝试[J].计算机教育,2025(1):9-10.

（完）