两端锚定的桥梁：入门计算机科学中的形式演绎与离散数学中的代码证明

标准本科计算机科学课程中编程与数学部分之间存在明显脱节，导致学生误解二者关联。我们提议在课程早期——具体在 CS1 与离散数学导论课中——以关于程序的形式化推理作为桥梁连接这两门课。本文报道了 Haverford 与 Grinnell 学院在构建 CS1 与离散数学之间此桥梁端点上的经验。Haverford 长期以来的“3-2-1”课程在介绍编程概念的同时引入代码推理，Grinnell 的离散数学则以代码推理作为逻辑与形式演绎的动机。两门课程均以编程语言界符号化代码执行技术为基础的风格呈现代码推理，但针对各自课程特点做了调整。这些课程主要依赖纸笔传统证明撰写方式。这对直到作业批改才获得反馈的学生，以及必须承担解读学生证明并给予有用反馈负担的教师而言并不理想。为此，我们也描述了 Orca 的当前状态——一个我们正在开发的面向本科教育的证明辅助工具，用于解决课程中的这些问题。最后，在教学过程中，我们发现了若干关于代码推理在弥合编程与数学鸿沟中有效性及诸如 \orca 类工具支持该教学法能力的教育研究问题。我们提出这些研究问题作为下一步，以形式化课程中的初步经验，期望最终推广我们的方法以供更广泛采用。