在一次派對上，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 的屬性。
這些事實和屬性的整體結構將被稱為進步。
在任何語言中，你最終都想對程式碼本身說些什麼。
就像這裡有一個總是回傳 5 的函式，但在幾乎沒有任何語言中，你無法真正以語言本身幫助你的方式來利用這個事實。
缺乏型別的語言 tend to grow them（傾向於發展出型別），例如 PHP 在 7.4 版本和 Python 的型別註解，以及普遍趨向 TypeScript 和 Rust 的發展。
不可避免地，人們想要推動型別的極限。即使是 Go 也是如此。C++ 的模板是終極的例子。如果它可以在編譯時計算，總有一天會有人想要，就像 Rust 持續進行的 const ification（常數化）。
但做任何事情最簡單的方式就是「正確地」做。正確地做基本上依賴於依賴型別。有比它們更花俏的東西，但就像圖靈完備性一樣，依賴型別可以讓你達到那個境界。因此，可完善。
在型別之上，你需要基礎設施來顯示兩個型別是否相等/不相等。這基本上是一個定理證明器。任何依賴型別的語言都可以變成一個定理證明器，但它需要發展出我們稱之為「定理證明基礎設施」的良好 API。
這是故事的一半。語義學的一半。語法學的一半是元程式設計和自訂語法。
大多數語言沒有這方面的設施，或者有點彆扭，例如 Rust 的程序宏。
Lean 的無縫整合令人驚豔。這裡是用自訂的棋盤符號表示的井字遊戲：
這讓你能夠分層設計 API，並將它們隱藏在語法後面。此外，語法的解釋可以輕鬆交換。Lean 的型別系統在元程式設計方面有所幫助（但我很樂見具有某種模態的元元程式設計，以便為 Lean 語法提供更好的基礎設施）。
正確地做這件事就是一個定理證明器。定理證明是程式設計中匯聚演化的結果。
這是最重要的一點。慢速的語言很糟糕。那為什麼還要使用電腦呢。
Lean 可以更快。它沒有 Rust 那麼快，但由於能夠顯示兩段程式碼相等，它具有很高的優化潛力。
Leo de Moura 似乎也確信這一點的必要性，足以讓向後相容性被拋諸腦後。幸運的是，在 AI 世界中，重寫程式碼要容易得多，而定理證明器是終極的重構工具（怎麼會不是呢？）
Lean 是其類別中唯一真正獲得關注的語言。Coq、Idris、Agda — 它們都不再真正競爭了。否則 Idris 可以算是一種真正的程式語言，同時也是證明器，但社群從未達到臨界質量。F* 也可以算，但其社群微不足道。Lean 是具有原始程式設計能力同時也是定理證明器的語言，而且它正在成長。
強大的元程式設計通常伴隨著詛咒。Lisp 的詛咒：它太容易讓你自行開發，以至於沒有人能完成任何事情。Mark Tarver 的經典說法是關於 Lisp 的 GUI — 9 個產品，沒有一個有文件，沒有一個沒有錯誤，每個人都對自己的作品感到滿意。公地的悲劇。
C/C++ 的方法則相反。用鑷子和膠水做任何事情都非常困難，以至於任何有意義的事情都是真正的成就。你需要文件。你需要幫助，所以你需要社交。你與他人合作才能有所成就。
形式化數學在「非常困難」這一點上與之完全相同，並且它團結了社群。mathlib 是大教堂。較小的專案是市集，市集將完成的工作回饋給 mathlib。這不是一個理論上的說法 — 它已經發生了。
Lean 是否也能擺脫軟體方面的詛咒還有待觀察。但數學家用戶群到目前為止也圍繞著共享的軟體需求團結起來：Lake、Elan、Reservoir、一個主導的標準函式庫。該語言有 Terence Tao、Peter Scholze 和 Leo de Moura 作為領導者可以依靠。這足以產生足夠的引力，讓大家朝同一個方向努力。