高級程式語言

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