Computer Science as Infrastructure: the Spine of the Lean Computer Science Library (CSLib)

想象一下数学的世界是一座宏伟而古老的城市。几个世纪以来，人们各自构建逻辑之屋，但由于他们经常使用不同的蓝图，导致工具难以共享，也难以共同建造新的街区。随后，Mathlib 出现了——这是一个宏大的、中心化的图书馆，全球的数学家们在此达成共识，使用相同的语言和规则来构建他们的证明。这就像是一个通用的数学翻译器，将复杂且孤立的思想转化为一个共享的、经过验证的城市景观，让每个人都能清晰地看到一座桥是如何建成的，并相信它不会坍塌。

现在，请想象计算机科学是等待被建造的下一个伟大城市。它是关于我们如何命令机器去思考、移动和解决问题的研究。但就像旧有的数学城市一样，计算机科学往往曾是一系列孤立的工作坊。本文介绍了 CSLib，这是一个新项目，旨在为计算机科学做它在数学领域所做过的事（即 Mathlib）：创建一个单一的、共享的家园，用于存放我们用来描述软件的所有规则、语言和模型。这里有一个简单却又巨大的问题：我们能否构建出计算机科学的“脊梁”，使其如此坚固且标准化，以至于我们可以像证明数学定理一样，对我们的软件和模型进行形式化验证？如果我们能做到这一点，就意味着我们可以构建具有数学验证属性的数字系统，而不是仅仅依赖测试来寻找错误。

数字城市的全新脊梁

将 CSLib 视为一个不断增长的数字城市的中央神经系统。正如一座城市需要坚固的脊梁来支撑起摩天大楼和桥梁一样，计算机科学也需要一个由经过验证的规则构成的坚实基础，来支撑我们每天使用的复杂软件。本文展示了这一脊梁的蓝图。它不仅仅是建造了几个随机的房间；它奠定了基本原则、运行规则以及语义框架（这只是一个高级说法，意指我们讨论计算机程序的“词典和语法”）——这是所有人在这座新图书馆中都将达成一致的准则。

作者们是在巨人的肩膀上构建这座图书馆，特别是遵循了 Mathlib 的足迹。他们采用了在纯数学领域取得成功的配方，并将其应用于杂乱且务实的计算机科学世界。其目标是创建一个场所，让关于编程语言和软件模型的想法可以被任何人、在任何地方存储、检查和复用。

行业工具

为了让这座图书馆发挥作用，本文介绍了一些巧妙的工具，它们充当了我们数字城市的建筑设备。

首先，他们构建了可复用的语义接口。想象一下，你正在尝试解释一个电子游戏角色是如何移动的。你可以描述每一帧动画，或者你可以使用一套标准的规则，例如“如果玩家按下‘A’键，角色就会跳跃”。在 CSLib 中，作者为两种特定类型的运动创建了标准“规则书”：归约（程序如何逐步简化自身）和标记转换系统（程序如何从一个状态转移到另一个状态，就像红绿灯从红灯变为绿灯一样）。这些不仅仅是单一的描述；它们是可复用的接口。这意味着如果你想证明一种新的编程语言，你不需要重新发明轮子。你只需要将你的新语言接入这些现有的、受信任的规则书即可。

其次，本文强调了证明自动化。在过去，证明一段软件是正确的就像是手动检查墙上的每一块砖头。这既缓慢又容易产生人为错误。作者贡献了充当超级快速机器人助手的工具。这种自动化有助于检查证明，确保逻辑成立，而无需人类盯着每一行代码。这就像拥有一个永不疲倦的逻辑拼写检查器。

第三，他们建立了 CI/测试支持。在软件领域，“CI”代表持续集成，这基本上是一种安全网。每当有人向库中添加新组件时，自动化系统都会检查它是否破坏了其他部分。本文指出，该系统旨在保持新的计算机科学库与旧的数学库（Mathlib）兼容。这就像是确保新的数字高速公路能完美连接到现有的数学桥梁，从而使交通能在两个世界之间流畅穿梭。

里面究竟有什么？

本文不仅讨论了工具，还展示了它们是如何被应用的。作者贡献了在该新框架下的语言和模型的首批实质性进展。这意味着他们不仅搭建了脚手架，还已经开始建造第一批建筑。他们将现实世界的编程语言和模型概念，利用他们的新系统成功进行了形式化。

然而，理解所取得成就的范围非常重要。本文将这些成果呈现为基础原则和初步发展。它表明这种方法是行之有效的，并为未来提供了坚实的框架，但它并不声称已经解决了计算机科学中的每一个问题。这项工作被描述为一个“快速增长”的库，暗示它是一个仍在建设中的、有生命力的项目。作者展示了基础是稳固的，第一批房间也已布置妥当，但这座城市远未完工。

为什么这很重要

那么，为什么一个好奇的青少年应该关心一个形式化的计算机科学库呢？因为这决定了你是用纸板盖房子，还是用钢铁盖房子。今天我们在编写软件时，通常通过测试来观察它是否会崩溃。如果它没崩，我们就假设它是安全的。但有了 CSLib，目标是创建一个共享的、经过验证的库，让软件的规则和模型能够受到严格的检查。通过集中这些想法并提供自动化检查工具，作者们正在为软件开发铺平道路，使关键属性可以通过数学进行验证。

本文认为，通过集中这些想法并提供自动化检查过程的工具，我们可以构建一个数字世界的“脊梁”坚不可摧的未来。这是一个充满趣味且雄心勃勃的愿景：通过数学的秩序来驯服编码的混沌，创造一个不仅功能完备，而且在根本上值得信赖的数字景观。