Why did IOG choose Haskell to build Cardano? | Cardano Explorer (cexplorer.io)
IOG 团队仔细决定了使用哪种编程语言和工具进行 Cardano 开发。 最终，他们选择了 Haskell。 该团队必须能够正式验证白皮书中所写的所有内容都与源代码正确对应。 快来看看团队是如何将白皮书中的数学证明转化为Haskell源代码的。
TLDR
在 Cardano 之前，前 10 名中没有一个项目使用形式化方法。
白皮书是正式规范的基础。 它是用 Haskell 编写的源代码的基础。
正式规范和 Haskell 源代码具有非常相似的符号。
从白皮书到源代码
区块链行业很多团队都有一种“move fast and break things”的创业心态。 这种心态是由年轻、贪婪和激情驱动的。 许多协议的源代码通常是在没有事先研究的情况下仓促编写的。 在某些情况下，我们可以谈论团队对用户不负责任的做法。 对立面是一种缓慢的、有条不紊的、以学术为导向的方法，其动机是希望巩固我们领域的创新。 在团队开始开发 Cardano 时，市值排名前 10 的加密货币都没有基于同行评审的协议，并且是根据正式规范实施的。 IOG 团队决定使用形式化方法来开发 Cardano。
IOG 团队在白皮书中定义并从数学上证明了协议和其他组件行为的正确性。 然后将这些用于创建正式规范。 形式规范是对系统行为和属性的精确的数学描述。
在白皮书中，数学符号用于表达抽象概念和数学证明。 它很精确，但非专家可能很难理解。 形式规范符号用于以精确的数学方式表达软件系统的行为和属性。 它不像数学符号那么抽象，但比源代码更精确。 换句话说，程序员可能不理解白皮书中使用的数学符号，但能够理解正式的规范。
在创建正式规范后，下一步是使用编程语言 Haskell 实现源代码。 预计实现遵循正式规范中描述的规范和属性。 实现应该以这样一种方式完成，即可以从数学上证明实现满足正式规范中描述的要求和属性。 换句话说，可以根据规范对源代码进行形式验证。
Haskell 源代码用于表达 Cardano 的实现。 它是预期行为的最具体形式。 它是系统执行的形式。 Haskell 源代码不如正式规范符号那么精确，但它更容易被 Haskell 开发人员理解。
虽然数学符号、形式规范符号和 Haskell 源代码之间存在联系，但在它们之间切换并不总是那么容易。 由于使用了不同的符号，因此它们的抽象级别和表达能力是不同的。 目标是最大化不同符号之间的信息传递。
科学家和数学家不必是 Haskell 程序员。 他们的工作是写一份白皮书。 Haskell 程序员不必是顶尖的数学家。 正式规范是两组之间的一种中介。 必须有人能够根据白皮书创建正式规范。 但是，可以使用可以在数学符号、形式规范符号和源代码之间自动转换的工具，例如依赖类型的编程语言，如 Coq 或 Agda。
Cog 和 Agda 都是形式化验证工具，可以在 Haskell 等函数式编程语言的上下文中使用。 它们都是证明助手，是帮助用户编写形式化数学证明的计算机程序。
Cog 和 Agda 都是基于使用形式化方法来增强软件系统的可靠性和正确性的思想。 Cog 更特定于并发算法，而 Agda 更通用，可用于任何类型的函数式编程。 它们都是确保软件系统正确性的有力工具，可以一起使用以提供全面的验证解决方案。
为什么选择 Haskell
Haskell 是一种函数式编程语言，非常适合在软件开发过程中使用形式化方法。
Haskell 的主要优点之一是它的强类型系统。 Haskell 有一个静态类型系统，这意味着在编译时检查类型，提供高级别的安全性并在程序运行之前防止许多类型的错误。 此外，Haskell 支持类型继承，这意味着程序员不需要明确指定变量和函数的类型，使代码更加简洁和可读。
在 Haskell 中，默认情况下变量是不可变的，这意味着一旦为变量赋值，就无法更改。 这使得推断程序的行为变得更加容易，并且可以简化并发和并行编程。 不变性还有助于防止因变量的意外更改而导致的错误，并使代码更易于测试。
Haskell 还非常关注函数式编程，它鼓励声明式和表达式的编程风格。 在函数式编程中，重点是描述程序应该做什么，而不是它应该如何做。 这使代码更具可读性和可维护性，并且可以简化调试和测试。
Haskell 的强类型系统和数学编程风格使其非常适合形式化方法。 Haskell 中的类型系统非常具有表现力，允许对代码进行高级静态检查。 这意味着可以在编译时捕获许多常见的编程错误，而不是在运行时。 此外，函数式编程范式鼓励数学思维方式，这有助于使代码更可预测且更易于推理。 它对于复杂的大型 Cardano 代码库尤其有益。
Haskell 的垃圾收集和严格的评估确保程序免受运行时错误的影响，例如空指针取消引用、缓冲区溢出和数据竞争。 这使得它更适合安全关键系统。
Haskell 的并发和并行模型基于轻量级线程和消息传递，可以轻松编写可以利用多核和处理器的代码。 这对于需要同时处理大量交易的区块链平台Cardano项目来说很重要。
Haskell 的高级抽象（例如 monad）使编写模块化、可组合和可重用的代码变得更加容易。 这有助于降低代码库的复杂性，并更容易推理和证明代码的属性。
阶乘函数
让我们看一个如何将数学符号转换为源代码的简单示例。
阶乘函数的完整数学证明如下所示：
有关阶乘函数，请参阅 Agda 中的正式规范：
查看阶乘函数的 Coq 表示法：
查看阶乘函数的 Haskell 源代码如何类似于 Agda 和 Coq 符号：
为了进行比较，请参阅传统 C++ 语言中阶乘函数的实现方式：
程序员需要理解正式规范才能用 Haskell 编写相应的源代码。 当然，程序员也可以用 C++ 编写阶乘函数，但请注意其表示法与正式规范不太相似。 两种情况下的代码都完全按照规范所说的去做，这是最重要的事情。
然而，对于程序员来说，比较 Haskell 符号和形式规范比他必须用 C++（或其他类似语言）做同样的事情更自然。 对于更复杂的功能，差异会更加明显。
结论
IOG 团队选择 Haskell 的原因有很多。 重要的不仅是语言本身，还有它解决特定问题的适用性、可用工具的数量以及优秀开发人员的数量。 普通程序员很少有使用形式化方法的经验。 对于 Haskell 程序员来说，频率更高。 此外，很难找到没有详细计算机科学知识的有经验的 Haskell 开发人员。
在需要使用形式化方法进行 Cardano 开发的背景下，Haskell 是自然而然的选择之一。 Cardano 正在构建为一个关键任务项目，而 Haskell 的 DNA 特性有助于实现这一目标。