Formality

具有正式证明的现代编程语言。 现在自己写！ 为什么要正式证明？ 当大多数人听到形式证明时，他们自然会想到数学和安全性，或“无聊的东西”。 虽然可以使用形式化证明来正式化定理并验证软件的正确性，但Formality的方法却有所不同：我们专注于将证明用作提高开发人员生产率的工具。 毫无疑问，将类型添加到非类型化语言中可以大大提高生产率，特别是当代码库增长到一定程度时：只需看看TypeScript的兴起。 形式证明在某种程度上是通用语言中使用的简单类型的演变。 我们认为，证明是等待探索的超级大国，正确使用证明可以以破坏性的方式提高开发人员的生产力：想想Haskell在类固醇上的骇客。 正式性旨在探索和启用形式证明的这一方面，我们将在不久后发布更多有关形式证明的信息。 为什么要正式？ 市场上有一些有趣的证明语言或通常称为的证明助手。 ， ， ， 等。 但是这些（在某些情况下，也许除我