函数式编程
函数式编程，它不像命令式编程那样，通过一连串的指令来改变程序的状态，而是像数学公式那样，通过函数来描述“是什么”。每一个函数都是确定的、有限的，给它同样的输入，它永远给你同样的输出，没有任何隐藏的副作用。这种特性使得程序员在编写代码时，无需担心函数内部会影响函数外部的数据，通过这一点，函数式编程可以极大程度上解决数据竞争的问题。
函数式编程鼓励我们使用不可变的数据和高阶的函数。数据一旦创建，便不会改变；新的数据只能由旧的数据通过函数计算而来。这就像我们在一张白纸上写写画画，但从不擦除，只是不断地在旁边添加新的推导。于是，循环被递归取代，变量赋值变成了参数传递，程序的控制流不再纠缠于复杂的状态变迁，而是回归到函数应用的简洁表达。这种表达方式带着一种朴素的数学美感，让人在阅读代码时，仿佛在读一篇层次分明的推理文章。
Coq 是一门基于类型论的形式化证明工具，它自带的函数式编程语言 Gallina，其内核比许多常见的函数式语言还要纯粹。在 Coq 里定义函数，你必须遵循严格的递归规则，以保证程序的终止和数学上的良基性。这不仅仅是为了写程序，更是为了在同一个语言框架里证明这个程序的性质。你写下一个对列表求和的函数，然后你立刻就可以写下并证明这个函数满足交换律、结合律。函数式编程的“函数”和数学上的“函数”在 Coq 中合二为一，代码即是证明的一部分，程序与证明如影随形。
类型论
类型论 是 Coq 的理论基础之一，它为程序和证明提供了统一的框架。在类型论中，类型不仅仅是对数据的分类，更是对程序行为的约束和描述。
理解类型的概念及其在编程语言中的作用是学习 Coq 的重要前提。类型可以看作是程序的“契约”，它规定了函数的输入和输出，确保程序在运行时不会出现类型错误。通过类型系统，程序员可以在编译阶段发现许多潜在的错误，从而提高程序的可靠性。
在 Coq 中，类型系统比许多常见的编程语言更为强大。它不仅支持简单类型系统，还支持依赖类型。依赖类型允许类型依赖于值，这使得我们可以在类型中表达更丰富的约束。例如，我们可以定义一个类型，表示“长度为 n 的列表”，从而在类型层面保证程序的正确性。
熟悉简单类型系统和依赖类型的基本原理，有助于理解 Coq 中的函数定义和证明构造。通过类型论，我们不仅可以描述程序的行为，还可以在同一个框架中证明程序的性质。
关于 Coq 复杂且怪异的语法
经过了两天的学习，我最终选择放弃了 Coq。这门语言确实非常强大，其理论基础和工具链在学术界享有极高的认可度。然而，它复杂且怪异的语法和策略规则让我很难说这是一个很好的工具。每一次尝试理解其证明策略时，我都感到自己在与一座陡峭的山峰较量。
相比之下，我发现 Lean 4 提供了一种更现代、更易于上手的体验。Lean 4 的语法更加直观，工具链也更贴近现代开发者的需求。虽然 Coq 的强大毋庸置疑，但在实际学习和使用中，我更愿意选择一门能够让我专注于逻辑推理和证明构造，而不是与语言本身的复杂性斗争的工具。因此，我决定转而拥抱 Lean 4，期待在这门语言中找到更高效的形式化证明之路。
所以之后的内容可能就会以记录 Lean 4 的学习记录为主了。