Vitalik：值得嘗試的新型高級編程語言應讓人更易閱讀定義和定理
來源：
x.com
Vitalik 在 X 平臺發文表示，一種值得嘗試的新型“高級編程語言”是編譯爲 Lean（或 HOL 等）的語言，重點是儘可能讓人類更容易閱讀定義和定理。 而不是證明，因爲證明只要正確即可，關鍵在於定義和定理本身。 其設想用途是，AI 輸出一大段證明，而讀者需要儘可能輕鬆地理解這些輸出中實際被證明了哪些精確主張。