Hacker News 中文摘要

文章摘要

文章认为Lean是最优秀的编程语言，因为它具有"可完善性"——虽然不完美，但允许用户在语言内部定义和验证代码属性。作者通过一个总是返回5的函数示例，展示了Lean如何支持对代码行为进行形式化验证，这是其他语言难以实现的特性。

文章总结

可臻完美的编程语言——Soter

在湾区的一次聚会上，Sydney Von Arx问我能否列举40种编程语言。这很符合湾区风格。我确实能列举出许多：Racket、Agda、Clean、Elm、TypeScript、sh、ASP、Verilog、JavaScript、Scheme、Rust、Nim、INTERCAL、sed、Isabelle、Visual Basic、zsh、Alokscript、Coq、Idris、Hack、Prolog、Whitespace、PureScript、Go、Odin、Haskell、Python、tcsh、Unison、Clingo、Bash、Java、Zig、Cyclone、PHP、awk、C、ActionScript、C++。

但Lean才是最佳选择。

为何选择Lean？

因为它具备"可完美性"。虽然尚未完美，但具有完善的潜力。你可以在Lean中描述关于Lean本身的属性，这些属性和事实的集合构成了所谓的"进步"。

在所有编程语言中，开发者最终都希望对代码本身进行描述。例如下面这个总是返回5的函数，但几乎没有语言能真正利用这一特性：

typescript function returnFive(x: number): number { return 5; }

而Lean可以做到：

```lean def returnFive (x : Int) : Int := 5

theorem returnFiveeqfive (x : Int) : returnFive x = 5 := rfl

example (a : Int) : 6 = returnFive a + 1 := by unfold returnFive rfl ```

无类型语言往往最终会引入类型系统，如PHP 7.4和Python的类型注解，以及TypeScript和Rust的流行趋势。人们总是希望扩展类型系统，比如C++模板和Rust的常量计算。

实现这一目标的最佳方式就是依赖类型。依赖类型就像图灵完备性一样强大，是实现语言完美性的关键。在此基础上，还需要类型等价证明的基础设施，这本质上就是一个定理证明器。任何依赖类型语言都可以成为定理证明器，但需要发展出我们称之为"定理证明基础设施"的友好API。

元编程

大多数语言要么缺乏元编程能力，要么实现方式笨拙（如Rust的过程宏）。而Lean的元编程能力异常强大。例如，我们可以为井字棋游戏创建自定义的棋盘表示法：

```lean inductive Player where | X | O inductive Square where | empty | occupied (player : Player)

@[simp] def boardSize : Nat := 9 structure Board where squares : Array Square ```

然后定义自定义语法：

```lean declaresyntaxcat tttCell syntax "X" : tttCell; syntax "O" : tttCell; syntax "_" : tttCell

declaresyntaxcat tttRow syntax tttCell "|" tttCell "|" tttCell : tttRow

declaresyntaxcat tttBoardSyntax syntax tttRow tttRow tttRow : tttBoardSyntax ```

这种能力允许开发者设计分层的API，并将其隐藏在语法背后。Lean的类型系统为元编程提供了支持（虽然我们期待未来能实现元元编程）。

性能

运行速度慢的语言令人难以接受。Lean虽然目前不如Rust快，但由于能够证明代码等价性，它具有极高的优化潜力。例如：

lean theorem five_plus_one_eq_six : ∀ a : Int, returnFive a + 1 = 6 := by intro a unfold returnFive rfl

Lean创始人Leo de Moura也认同这一方向，甚至不惜牺牲向后兼容性。在AI时代，代码重写变得更容易，而定理证明器正是终极的重构工具。

社区生态

在其同类语言中，Lean是唯一真正获得发展势头的。Coq、Idris、Agda等已不再具有竞争力。Idris本可以成为兼具编程语言和证明器特性的选择，但其社区未能达到临界规模。F*的社区规模更小。Lean是既具备实际编程能力又是定理证明器，并且正在蓬勃发展的语言。

这篇文章本身就是用Lean代码写成的。

（注：最后一段关于Eliza Zhang的轶事与主题无关，已省略）

评论总结

以下是评论内容的总结：

对Lean语言的评价
- 正面评价：Lean4被赞为"best in class functional programming language"，具有惊人的表达能力（"astonishingly expressive"）。
  引用："i love lean4, best in class functional programming language" (评论5)
  引用："Lean is astonishingly expressive." (评论11)
- 负面评价：Lean4的体积从Lean3的15MB膨胀到2.5GB，且存在稳定性问题。
  引用："Lean 4 is the most bloated among this Big Three" (评论8)
  引用："the last update broke unification in a strange way" (评论8)
类型系统的争议
- 支持类型：有人认为类型系统是语言发展的必然趋势，如PHP和Python的类型注释。
- 反对类型：有人认为类型系统并非必需，如Ruby和Clojure的例子。
  引用："clojure exists as an example of people trying types and then realising it's cruft" (评论14)
  引用："Not everyone shares that opinion. See ruby." (评论13)
技术细节讨论
- 对博客技术实现的好奇：有人对博客用Lean代码实现表示兴趣。
  引用："wait, I'm intrigued, it says the blog itself is lean code. How?" (评论6)
- 安装方式的调侃：对通过VS Code安装Lean的方式表示幽默。
  引用："Lol" (评论7)
其他观点
- 文档体验：有人喜欢网站提供的悬停文档功能。
  引用："i like this website, it shows documentation when hovering the code" (评论2)
- 语言选择：有人列出多种编程语言，表达对语言多样性的兴趣。
  引用："Fun challenge. Unlike the author, I have nothing really to add." (评论4)

总结：评论中对Lean语言有褒贬不一的评价，类型系统的必要性引发争议，同时也有对技术细节和语言选择的讨论。

可完善的编程语言 -- A perfectable programming language